sq_injective — Mathlib

English

In a commutative ring R with Char 2 and no zero-divisors, the map x ↦ x^2 is injective.

Русский

В коммутативном кольце R с Char 2 и без делителей нуля отображение x ↦ x^2 инъективно.

LaTeX

$$∀ {R} [CommRing R] [CharP R 2] [NoZeroDivisors R], Function.Injective (λ x: R, x^2)$$

Lean4

theorem sq_injective : Function.Injective fun x : R ↦ x ^ 2 :=
  by
  intro x y h
  rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h

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