four — Mathlib

English

In any AddMonoidWithOne α with a compatible order and the usual positivity assumptions, the numeral 4 is nonzero; equivalently, (4 : α) ≠ 0.

Русский

В любой AddMonoidWithOne α с подходящим порядком и обычными условиями неотрицательности единицы, число 4 не равно нулю; то есть (4 : α) ≠ 0.

LaTeX

$$$(4 : \alpha) \neq 0$$$

Lean4

instance four : NeZero (4 : α) :=
  ⟨zero_lt_four.ne'⟩

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