mul_inv_le_one

Mathlib.Algebra.Order.Monoid.Unbundled.Units

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

English

Let M be a monoid with order and MulRightMono; for a unit u, a * u⁻¹ ≤ 1 iff a ≤ u.

Русский

Пусть M — моноид с порядком и MulRightMono; для единицы u: a · u⁻¹ ≤ 1 эквивалентно a ≤ u.

LaTeX

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

Lean4

theorem mul_inv_le_one : a * u⁻¹ ≤ 1 ↔ a ≤ u := by rw [u.mul_inv_le_iff, one_mul]

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

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

Разделы

Аффилиация

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