one_lt_iff_ne_one

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

In a canonically ordered multiplicative monoid, 1 < a if a ≠ 1.

Русский

В канонически упорядоченном мультипликативном моноиде, если a ≠ 1, то 1 < a.

LaTeX

$$$ a \\neq 1 \\rightarrow 1 < a $$$

Lean4

@[to_additive]
theorem one_lt_iff_ne_one : 1 < a ↔ a ≠ 1 :=
  (one_le a).lt_iff_ne.trans ne_comm

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

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

Разделы

Аффилиация

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