M : Type u_1
N : Type ?u.155571
G : Type ?u.155574
R : Type ?u.155577
S : Type ?u.155580
F : Type ?u.155583
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k✝ l k : ℕ+
ζ : Mˣ
⊢ ζ ^ ↑k = 1 ↔ ↑ζ ^ ↑k = 1
M : Type u_1
N : Type ?u.155571
G : Type ?u.155574
R : Type ?u.155577
S : Type ?u.155580
F : Type ?u.155583
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k✝ l k : ℕ+
ζ : Mˣ
⊢ ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ ↑k = 1
rw [mem_rootsOfUnity]
no goals
M : Type u_1
N : Type ?u.155571
G : Type ?u.155574
R : Type ?u.155577
S : Type ?u.155580
F : Type ?u.155583
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k✝ l k : ℕ+
ζ : Mˣ
⊢ ζ ^ ↑k = 1 ↔ ↑ζ ^ ↑k = 1
norm_cast