case pos
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Nat.coprime i k
h0 : k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k

case neg
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Nat.coprime i k
⊢ IsPrimitiveRoot (ζ ^ i) k
by_cases h0 : k = 0
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑ζ ^ i) k
case neg
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k
rcases h.isUnit (Nat.pos_of_ne_zero h0) with ⟨ζ, rfl⟩
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑ζ ^ i) k
rw [← Units.val_pow_eq_pow_val]
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (ζ ^ i) k
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k
rw [coe_units_iff] at h ⊢
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ ∀ (l : ℕ), (ζ ^ i) ^ l = 1 → k ∣ l
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (ζ ^ i) k
refine'
  { pow_eq_one := by rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]
    dvd_of_pow_eq_one := _ }
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ k ∣ l
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ ∀ (l : ℕ), (ζ ^ i) ^ l = 1 → k ∣ l
intro l hl
case neg.intro.a
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ l = 1
case neg.intro
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ k ∣ l
apply h.dvd_of_pow_eq_one
case neg.intro.a
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * Nat.gcdA i k) * (ζ ^ (↑k * Nat.gcdB i k)) ^ l = 1
case neg.intro.a
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ l = 1
rw [← pow_one ζ, ← zpow_ofNat ζ, ← hi.gcd_eq_one, Nat.gcd_eq_gcd_ab, zpow_add, mul_pow,
  ← zpow_ofNat, ← zpow_mul, mul_right_comm]
no goals
case neg.intro.a
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * Nat.gcdA i k) * (ζ ^ (↑k * Nat.gcdB i k)) ^ l = 1
simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_ofNat]
case pos
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
l : ℕ
ζ : M
f : F
i : ℕ
h : IsPrimitiveRoot ζ 0
hi : Nat.coprime i 0
⊢ IsPrimitiveRoot (ζ ^ i) 0
case pos
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Nat.coprime i k
h0 : k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k
subst k
no goals
case pos
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
l : ℕ
ζ : M
f : F
i : ℕ
h : IsPrimitiveRoot ζ 0
hi : Nat.coprime i 0
⊢ IsPrimitiveRoot (ζ ^ i) 0
simp_all only [pow_one, Nat.coprime_zero_right]
no goals
M : Type u_1
N : Type ?u.1908173
G : Type ?u.1908176
R : Type ?u.1908179
S : Type ?u.1908182
F : Type ?u.1908185
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
i : ℕ
hi : Nat.coprime i k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ (ζ ^ i) ^ k = 1
rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]