mul_inv_le_iff

Mathlib.Algebra.Order.Monoid.Unbundled.Units

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_inv_le_iff : a * u⁻¹ ≤ b ↔ a ≤ b * u := by rw [← u.mul_le_mul_iff_right, u.inv_mul_cancel_right]

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

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

Разделы

Аффилиация

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