inv_le_one

Mathlib.Algebra.Order.Monoid.Unbundled.Units

URI: https://scilib.ai/kg/mathlib#Units.inv_le_one

English

Let M be a monoid with order and MulLeftMono, and u ∈ Mˣ. Then u⁻¹ ≤ 1 iff 1 ≤ u.

Русский

Пусть M — моноид с порядком и слева монотонным умножением, и u ∈ Mˣ. Тогда u⁻¹ ≤ 1 эквивалентно 1 ≤ u.

LaTeX

$$$u^{-1} \le 1 \iff 1 \le u$$$

Lean4

@[simp]
theorem inv_le_one : u⁻¹ ≤ (1 : M) ↔ (1 : M) ≤ u := by rw [← u.mul_le_mul_iff_left, mul_one, mul_inv]

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

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

Разделы

Аффилиация

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