no goals
M : Type ?u.2706015
N : Type ?u.2706018
G : Type u_1
R : Type ?u.2706024
S : Type ?u.2706027
F : Type ?u.2706030
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ⁻¹ ^ k = 1
simp only [h.pow_eq_one, inv_one, eq_self_iff_true, inv_pow]
M : Type ?u.2706015
N : Type ?u.2706018
G : Type u_1
R : Type ?u.2706024
S : Type ?u.2706027
F : Type ?u.2706030
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ k ∣ l
M : Type ?u.2706015
N : Type ?u.2706018
G : Type u_1
R : Type ?u.2706024
S : Type ?u.2706027
F : Type ?u.2706030
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ∀ (l : ℕ), ζ⁻¹ ^ l = 1 → k ∣ l
intro l hl
M : Type ?u.2706015
N : Type ?u.2706018
G : Type u_1
R : Type ?u.2706024
S : Type ?u.2706027
F : Type ?u.2706030
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ ζ ^ l = 1
M : Type ?u.2706015
N : Type ?u.2706018
G : Type u_1
R : Type ?u.2706024
S : Type ?u.2706027
F : Type ?u.2706030
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ k ∣ l
apply h.dvd_of_pow_eq_one l
no goals
M : Type ?u.2706015
N : Type ?u.2706018
G : Type u_1
R : Type ?u.2706024
S : Type ?u.2706027
F : Type ?u.2706030
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ ζ ^ l = 1
rw [← inv_inj, ← inv_pow, hl, inv_one]