val_set_image_rootsOfUnity_two — Mathlib

English

Under a commutative ring with no zero divisors, the 2nd roots of unity map to {1, -1} by the unit embedding.

Русский

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

LaTeX

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

Lean4

theorem val_set_image_rootsOfUnity_two [CommRing R] [NoZeroDivisors R] :
    ((↑) : Rˣ → R) '' (rootsOfUnity 2 R) = {1, -1} := by
  ext x
  simp

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