isStrictlyPositive_one — Mathlib

English

One is strictly positive in any ordered semiring with appropriate structure.

Русский

Единица строго положительна во всяком упорядоченном полугруппе/кольце с нужной структурой.

LaTeX

$$$ \\mathrm{IsStrictlyPositive}(1) $$$

Lean4

@[simp, grind]
theorem _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] : IsStrictlyPositive (1 : A) :=
  iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩

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