mul_inv_le_iff_le_mul'

Mathlib.Algebra.Order.Group.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#mul_inv_le_iff_le_mul'

English

In a commutative group with a left-monoid property, a * b^{-1} ≤ c * d^{-1} is equivalent to a * d ≤ c * b.

Русский

В коммутативной группе с левой монотонностью: a b^{-1} ≤ c d^{-1} эквивалентно a d ≤ c b.

LaTeX

$$$a b^{-1} \le c d^{-1} \iff a d \le c b$$$

Lean4

@[to_additive]
theorem mul_inv_le_iff_le_mul' : a * b⁻¹ ≤ c ↔ a ≤ b * c := by rw [← inv_mul_le_iff_le_mul, mul_comm]

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

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

Разделы

Аффилиация

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