val_set_image_rootsOfUnity_one — Mathlib

English

In a commutative ring with no zero divisors, the image of the units under the embedding to R of the 2nd roots of unity is exactly {1, -1}.

Русский

В коммутативном кольце без нулевых делителей образ 2-ых корней единицы совпадает с {1, -1}.

LaTeX

$$$((\uparrow) : R^{\times} \to R)''(\operatorname{rootsOfUnity}_2(R)) = \{1,-1\}$$$

Lean4

theorem val_set_image_rootsOfUnity_one : ((↑) : Rˣ → R) '' (rootsOfUnity 1 R) = { 1 } :=
  by
  ext x
  simp

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