no goals
M : Type ?u.1340998
N : Type ?u.1341001
G : Type ?u.1341004
R : Type u_1
S : Type ?u.1341010
F : Type ?u.1341013
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k✝ l : ℕ+
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k : ℕ
m : ℕ+
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
ζ : Rˣ
⊢ ζ ∈ rootsOfUnity ({ val := p, property := (_ : 0 < p) } ^ k * m) R ↔ ζ ∈ rootsOfUnity m R
simp only [mem_rootsOfUnity', PNat.mul_coe, PNat.pow_coe, PNat.mk_coe,
  CharP.pow_prime_pow_mul_eq_one_iff]