pos

Mathlib.Algebra.Order.Monoid.Canonical.Defs

URI: https://scilib.ai/kg/mathlib#NeZero.pos

English

If a is nonzero in an AddZeroClass with a canonically ordered addition, then 0 < a.

Русский

Если a не равно нулю в аддитивном канонически упорядоченном классе AddZero, то 0 < a.

LaTeX

$$0 < a$$

Lean4

theorem pos {M} [AddZeroClass M] [PartialOrder M] [CanonicallyOrderedAdd M] (a : M) [NeZero a] : 0 < a :=
  (zero_le a).lt_of_ne <| NeZero.out.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru