M : Type u_1
N : Type ?u.2067990
G : Type ?u.2067993
R : Type ?u.2067996
S : Type ?u.2067999
F : Type ?u.2068002
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ ζ ^ l ≠ 1
M : Type u_1
N : Type ?u.2067990
G : Type ?u.2067993
R : Type ?u.2067996
S : Type ?u.2067999
F : Type ?u.2068002
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
hk : 0 < k
⊢ IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
refine' ⟨fun h => ⟨h.pow_eq_one, fun l hl' hl => _⟩,
  fun ⟨hζ, hl⟩ => IsPrimitiveRoot.mk_of_lt ζ hk hζ hl⟩
M : Type u_1
N : Type ?u.2067990
G : Type ?u.2067993
R : Type ?u.2067996
S : Type ?u.2067999
F : Type ?u.2068002
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1
M : Type u_1
N : Type ?u.2067990
G : Type ?u.2067993
R : Type ?u.2067996
S : Type ?u.2067999
F : Type ?u.2068002
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ ζ ^ l ≠ 1
rw [h.eq_orderOf] at hl
no goals
M : Type u_1
N : Type ?u.2067990
G : Type ?u.2067993
R : Type ?u.2067996
S : Type ?u.2067999
F : Type ?u.2068002
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1
exact pow_ne_one_of_lt_orderOf' hl'.ne' hl