M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R ∧ ∀ (x : R), x ∈ primitiveRoots 1 R → x = 1
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 1 R = {1}
apply Finset.eq_singleton_iff_unique_mem.2
case left
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R

case right
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∀ (x : R), x ∈ primitiveRoots 1 R → x = 1
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R ∧ ∀ (x : R), x ∈ primitiveRoots 1 R → x = 1
constructor
no goals
case left
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R
simp only [IsPrimitiveRoot.one_right_iff, mem_primitiveRoots zero_lt_one]
case right
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1
case right
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∀ (x : R), x ∈ primitiveRoots 1 R → x = 1
intro x hx
case right
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x = 1
⊢ x = 1
case right
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1
rw [mem_primitiveRoots zero_lt_one, IsPrimitiveRoot.one_right_iff] at hx
no goals
case right
M : Type ?u.2760785
N : Type ?u.2760788
G : Type ?u.2760791
R : Type u_1
S : Type ?u.2760797
F : Type ?u.2760800
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
ζ : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x = 1
⊢ x = 1
exact hx