M : Type ?u.2599937
N : Type ?u.2599940
G : Type u_1
R : Type ?u.2599946
S : Type ?u.2599949
F : Type ?u.2599952
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ ^ k = 1
M : Type ?u.2599937
N : Type ?u.2599940
G : Type u_1
R : Type ?u.2599946
S : Type ?u.2599949
F : Type ?u.2599952
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ ^ ↑k = 1
rw [zpow_ofNat]
no goals
M : Type ?u.2599937
N : Type ?u.2599940
G : Type u_1
R : Type ?u.2599946
S : Type ?u.2599949
F : Type ?u.2599952
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ ^ k = 1
exact h.pow_eq_one