two_ne_zero — Mathlib

English

In a nontrivial ring whose characteristic is not 2, 2 is nonzero.

Русский

В неквадратном кольце с характеристикой, не равной 2, 2 не равно нулю.

LaTeX

$$$ \text{ringChar}(R) \neq 2 \Rightarrow (2 : R) \neq 0 $$$

Lean4

/-- We have `2 ≠ 0` in a nontrivial ring whose characteristic is not `2`. -/
protected theorem two_ne_zero {R : Type*} [NonAssocSemiring R] [Nontrivial R] (hR : ringChar R ≠ 2) : (2 : R) ≠ 0 :=
  by
  rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]
  exact mt (or_iff_left hR).mp CharP.ringChar_ne_one

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