mem_rootsOfUnity_iff_mem_nthRoots

English

An nth root of unity in R× is in rootsOfUnity_k(R) if and only if its underlying element is in nthRoots_k(1).

Русский

Корень единицы порядка k в R× принадлежит корням единицы если и только если соответствующий элемент принадлежит k-й множеству nthRoots(1).

LaTeX

$$$\zeta \in rootsOfUnity(k,R) \iff (\zeta \colon R) \in nthRoots(k,1)$$$

Lean4

theorem mem_rootsOfUnity_iff_mem_nthRoots {ζ : Rˣ} : ζ ∈ rootsOfUnity k R ↔ (ζ : R) ∈ nthRoots k (1 : R) := by
  simp only [mem_rootsOfUnity, mem_nthRoots (NeZero.pos k), Units.ext_iff, Units.val_one, Units.val_pow_eq_pow_val]

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