le_one_iff_eq_one

Mathlib.Algebra.Order.Monoid.Canonical.Defs

URI: https://scilib.ai/kg/mathlib#le_one_iff_eq_one

English

For a canonically ordered monoid, a ≤ 1 if and only if a = 1.

Русский

Для канонически упорядоченного моноида: a ≤ 1 тогда и только тогда, когда a = 1.

LaTeX

$$$ a \\le 1 \\leftrightarrow a = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem le_one_iff_eq_one : a ≤ 1 ↔ a = 1 :=
  (one_le a).ge_iff_eq'

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

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

Разделы

Аффилиация

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