M✝ : Type ?u.1875140
N✝ : Type ?u.1875143
G : Type ?u.1875146
R : Type ?u.1875149
S : Type ?u.1875152
F : Type ?u.1875155
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N✝
inst✝³ : DivisionCommMonoid G
k l : ℕ
ζ✝ : M✝
f : F
h : IsPrimitiveRoot ζ✝ k
M : Type u_1
B : Type u_2
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : { x // x ∈ N }
⊢ (↑ζ ^ k = 1 ∧ ∀ (l : ℕ), ↑ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
M✝ : Type ?u.1875140
N✝ : Type ?u.1875143
G : Type ?u.1875146
R : Type ?u.1875149
S : Type ?u.1875152
F : Type ?u.1875155
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N✝
inst✝³ : DivisionCommMonoid G
k l : ℕ
ζ✝ : M✝
f : F
h : IsPrimitiveRoot ζ✝ k
M : Type u_1
B : Type u_2
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : { x // x ∈ N }
⊢ IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
simp_rw [iff_def]
no goals
M✝ : Type ?u.1875140
N✝ : Type ?u.1875143
G : Type ?u.1875146
R : Type ?u.1875149
S : Type ?u.1875152
F : Type ?u.1875155
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N✝
inst✝³ : DivisionCommMonoid G
k l : ℕ
ζ✝ : M✝
f : F
h : IsPrimitiveRoot ζ✝ k
M : Type u_1
B : Type u_2
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : { x // x ∈ N }
⊢ (↑ζ ^ k = 1 ∧ ∀ (l : ℕ), ↑ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
norm_cast