mem_rootsOfUnity_prime_pow_mul_iff'

English

A variant expressing ζ^(p^k·m) = 1 is equivalent to ζ ∈ rootsOfUnity m R under ExpChar p.

Русский

Замена ζ^(p^k·m) = 1 эквивалентна ζ ∈ rootsOfUnity m R при ExpChar p.

LaTeX

$$$\zeta^{p^k m} = 1 \iff \zeta ∈ rootsOfUnity(m)R$$$

Lean4

/-- A variant of `mem_rootsOfUnity_prime_pow_mul_iff` in terms of `ζ ^ _` -/
@[simp]
theorem mem_rootsOfUnity_prime_pow_mul_iff' (p k : ℕ) (m : ℕ) [ExpChar R p] {ζ : Rˣ} :
    ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R := by rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]

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