neg_one_ne_one_of_char_ne_two — Mathlib

English

Characteristic not equal to 2 in a domain implies that -1 ≠ 1.

Русский

Характеристика ≠ 2 в домене означает, что -1 ≠ 1.

LaTeX

$$$ ringChar\ R \neq 2 \rightarrow (-1 : R) \neq 1 $$$

Lean4

/-- Characteristic `≠ 2` and nontrivial implies that `-1 ≠ 1`. -/
theorem neg_one_ne_one_of_char_ne_two {R : Type*} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) :
    (-1 : R) ≠ 1 := fun h => Ring.two_ne_zero hR (one_add_one_eq_two (R := R) ▸ neg_eq_iff_add_eq_zero.mp h)

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