case intro
M : Type u_1
N : Type ?u.1660609
G : Type ?u.1660612
R : Type ?u.1660615
S : Type ?u.1660618
F : Type ?u.1660621
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ζ ^ (k * i) = 1
M : Type u_1
N : Type ?u.1660609
G : Type ?u.1660612
R : Type ?u.1660615
S : Type ?u.1660618
F : Type ?u.1660621
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ k ∣ l → ζ ^ l = 1
rintro ⟨i, rfl⟩
no goals
case intro
M : Type u_1
N : Type ?u.1660609
G : Type ?u.1660612
R : Type ?u.1660615
S : Type ?u.1660618
F : Type ?u.1660621
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ζ ^ (k * i) = 1
simp only [pow_mul, h.pow_eq_one, one_pow, PNat.mul_coe]