mem_rootsOfUnity_prime_pow_mul_iff

English

In ExpChar setting, membership of a root of unity of order p^k·m in R implies membership in rootsOfUnity m(R), and vice versa.

Русский

При заданном ExpChar p членство корня единицы порядка p^k·m в R равно членству в корнях единицы порядка m.

LaTeX

$$$\zeta ∈ rootsOfUnity(p^k \cdot m)\,R \iff \\zeta ∈ rootsOfUnity(m)\,R$$$

Lean4

theorem mem_rootsOfUnity_prime_pow_mul_iff (p k : ℕ) (m : ℕ) [ExpChar R p] {ζ : Rˣ} :
    ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R := by
  simp only [mem_rootsOfUnity', ExpChar.pow_prime_pow_mul_eq_one_iff]

Похожие утверждения