div_lt_div_right'

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

If a < b in a group, then a/c < b/c for any c.

Русский

Если a < b в группе, то для любого c выполняется a/c < b/c.

LaTeX

$$$a < b \implies \dfrac{a}{c} < \dfrac{b}{c}$$$

Lean4

@[to_additive (attr := gcongr) sub_lt_sub_right]
theorem div_lt_div_right' (h : a < b) (c : α) : a / c < b / c :=
  (div_lt_div_iff_right c).2 h

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

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

Разделы

Аффилиация

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