instNontrivialOfCharZero — Mathlib

English

If α is an additive monoid with one and has characteristic zero, then α is nontrivial; in particular 1 ≠ 0.

Русский

Если α обладает структурой аддитивного моноида с единицей и характеристика α равна нулю, то α неизотривиален; в частности 1 ≠ 0.

LaTeX

$$$1 \neq 0$$$

Lean4

instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α where
  exists_pair_ne := ⟨1, 0, (Nat.cast_one (R := α) ▸ Nat.cast_ne_zero.2 (by decide))⟩

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