charZero_one — Mathlib

English

In any additive monoid with one element and of characteristic zero, the element 1 is nonzero.

Русский

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

LaTeX

$$$\\mathrm{NeZero}(1)\\quad\\text{in CharZero}$$$

Lean4

instance charZero_one {M} [AddMonoidWithOne M] [CharZero M] : NeZero (1 : M) where
  out := by
    rw [← Nat.cast_one, Nat.cast_ne_zero]
    trivial

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