div_le_div_iff_right

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

For a,b,c in a group, a / c ≤ b / c is equivalent to a ≤ b.

Русский

Для группы: a / c ≤ b / c эквивалентно a ≤ b.

LaTeX

$$$a / c \le b / c \iff a \le b$$$

Lean4

@[to_additive]
theorem div_le_div_iff_right (c : α) : a / c ≤ b / c ↔ a ≤ b := by
  simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _

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

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

Разделы

Аффилиация

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