M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ¬ζ = 1

M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ζ ^ 2 = 1 ^ 2
M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ζ = -1
apply (eq_or_eq_neg_of_sq_eq_sq ζ 1 _).resolve_left
M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ¬ζ ^ 1 = 1
M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ¬ζ = 1
rw [← pow_one ζ]
no goals
M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ¬ζ ^ 1 = 1
apply h.pow_ne_one_of_pos_of_lt <;> decide
no goals
M : Type ?u.2771838
N : Type ?u.2771841
G : Type ?u.2771844
R : Type u_1
S : Type ?u.2771850
F : Type ?u.2771853
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ζ ^ 2 = 1 ^ 2
simp only [h.pow_eq_one, one_pow]