val_set_image_rootsOfUnity — Mathlib

English

For a commutative monoid R, the image of roots of unity under the unit map covers exactly the elements z ∈ R with z^k = 1.

Русский

Для коммутативного моноида R образ корней единства под картой единиц совпадает с множеством элементов z∈R, удовлетворяющих z^k=1.

LaTeX

$$$\operatorname{Image} (\text{Units}.val) (\operatorname{rootsOfUnity}_k(R)) = \{ z \in R \mid z^k = 1\}$$$

Lean4

@[simp]
theorem val_set_image_rootsOfUnity [NeZero k] : ((↑) : Rˣ → _) '' (rootsOfUnity k R) = {z : R | z ^ k = 1} :=
  by
  ext x
  exact
    ⟨fun ⟨y, hy1, hy2⟩ => by rw [← hy2]; exact (mem_rootsOfUnity' k y).mp hy1, fun h ↦
      ⟨(rootsOfUnity.mkOfPowEq x h), ⟨Subtype.coe_prop (rootsOfUnity.mkOfPowEq x h), rfl⟩⟩⟩

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