M : Type u_1
N : Type ?u.1712947
G : Type ?u.1712950
R : Type ?u.1712953
S : Type ?u.1712956
F : Type ?u.1712959
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ ζ * ζ ^ (k - 1) = 1
M : Type u_1
N : Type ?u.1712947
G : Type ?u.1712950
R : Type ?u.1712953
S : Type ?u.1712956
F : Type ?u.1712959
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ IsUnit ζ
apply isUnit_of_mul_eq_one ζ (ζ ^ (k - 1))
no goals
M : Type u_1
N : Type ?u.1712947
G : Type ?u.1712950
R : Type ?u.1712953
S : Type ?u.1712956
F : Type ?u.1712959
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ ζ * ζ ^ (k - 1) = 1
rw [← pow_succ, tsub_add_cancel_of_le h0.nat_succ_le, h.pow_eq_one]