neg_one_eq_one_iff — Mathlib

English

In a commutative ring with Char 2 and no zero divisors, the square map is injective.

Русский

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

LaTeX

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

Lean4

theorem neg_one_eq_one_iff [Nontrivial R] : (-1 : R) = 1 ↔ ringChar R = 2 :=
  by
  refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
  rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
  exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

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