iff_of_unital

Mathlib.Algebra.Algebra.StrictPositivity

URI: https://scilib.ai/kg/mathlib#IsStrictlyPositive.iff_of_unital

English

IsStrictlyPositive a is equivalent to 0 ≤ a and IsUnit a, in the unital setting.

Русский

IsStrictlyPositive a эквивалентно 0 ≤ a и IsUnit a в унитной структуре.

LaTeX

$$$ \\mathrm{IsStrictlyPositive}(a) \\iff (0 \\le a \\wedge \\mathrm{IsUnit}(a)). $$$

Lean4

@[grind =]
theorem iff_of_unital [LE A] [Monoid A] [Zero A] {a : A} : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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