case intro
M : Type u_1
N : Type ?u.364389
G : Type ?u.364392
R : Type ?u.364395
S : Type ?u.364398
F : Type ?u.364401
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k d : ℕ+
⊢ rootsOfUnity k M ≤ rootsOfUnity (k * d) M
M : Type u_1
N : Type ?u.364389
G : Type ?u.364392
R : Type ?u.364395
S : Type ?u.364398
F : Type ?u.364401
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ+
h : k ∣ l
⊢ rootsOfUnity k M ≤ rootsOfUnity l M
obtain ⟨d, rfl⟩ := h
case intro
M : Type u_1
N : Type ?u.364389
G : Type ?u.364392
R : Type ?u.364395
S : Type ?u.364398
F : Type ?u.364401
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k d : ℕ+
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M
case intro
M : Type u_1
N : Type ?u.364389
G : Type ?u.364392
R : Type ?u.364395
S : Type ?u.364398
F : Type ?u.364401
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k d : ℕ+
⊢ rootsOfUnity k M ≤ rootsOfUnity (k * d) M
intro ζ h
no goals
case intro
M : Type u_1
N : Type ?u.364389
G : Type ?u.364392
R : Type ?u.364395
S : Type ?u.364398
F : Type ?u.364401
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k d : ℕ+
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M
simp_all only [mem_rootsOfUnity, PNat.mul_coe, pow_mul, one_pow]