case intro.intro
M : Type u_1
N : Type u_2
G : Type ?u.365670
R : Type ?u.365673
S : Type ?u.365676
F : Type ?u.365679
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k✝ l : ℕ+
f : Mˣ →* Nˣ
k : ℕ+
ζ : Mˣ
h : ζ ∈ ↑(rootsOfUnity k M)
⊢ ↑f ζ ∈ rootsOfUnity k N
M : Type u_1
N : Type u_2
G : Type ?u.365670
R : Type ?u.365673
S : Type ?u.365676
F : Type ?u.365679
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k✝ l : ℕ+
f : Mˣ →* Nˣ
k : ℕ+
⊢ Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N
rintro _ ⟨ζ, h, rfl⟩
no goals
case intro.intro
M : Type u_1
N : Type u_2
G : Type ?u.365670
R : Type ?u.365673
S : Type ?u.365676
F : Type ?u.365679
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k✝ l : ℕ+
f : Mˣ →* Nˣ
k : ℕ+
ζ : Mˣ
h : ζ ∈ ↑(rootsOfUnity k M)
⊢ ↑f ζ ∈ rootsOfUnity k N
simp_all only [← map_pow, mem_rootsOfUnity, SetLike.mem_coe, MonoidHom.map_one]