M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
⊢ IsPrimitiveRoot ζ 1 ↔ ζ = 1
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ζ 1 ↔ ζ = 1
clear h
case mp
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
⊢ IsPrimitiveRoot ζ 1 → ζ = 1

case mpr
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
⊢ ζ = 1 → IsPrimitiveRoot ζ 1
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
⊢ IsPrimitiveRoot ζ 1 ↔ ζ = 1
constructor
case mp
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ 1
⊢ ζ = 1
case mp
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
⊢ IsPrimitiveRoot ζ 1 → ζ = 1
intro h
no goals
case mp
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h : IsPrimitiveRoot ζ 1
⊢ ζ = 1
rw [← pow_one ζ, h.pow_eq_one]
case mpr
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
⊢ IsPrimitiveRoot 1 1
case mpr
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
⊢ ζ = 1 → IsPrimitiveRoot ζ 1
rintro rfl
no goals
case mpr
M : Type u_1
N : Type ?u.1873978
G : Type ?u.1873981
R : Type ?u.1873984
S : Type ?u.1873987
F : Type ?u.1873990
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
f : F
⊢ IsPrimitiveRoot 1 1
exact one