sq_inj

Mathlib.Algebra.CharP.Two

URI: https://scilib.ai/kg/mathlib#CharTwo.CommRing.sq_inj

English

In a Char 2 commutative ring with no zero divisors, x^2 = y^2 if and only if x = y.

Русский

В коммутативном кольце с характеристикой 2 без делителей нуля, x^2 = y^2 эквивалентно x = y.

LaTeX

$$∀ {R} [CommRing R] [CharP R 2] [NoZeroDivisors R] {x y : R}, x^2 = y^2 ↔ x = y$$

Lean4

@[scoped simp]
theorem sq_inj {x y : R} : x ^ 2 = y ^ 2 ↔ x = y :=
  sq_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru