div_lt_div_left'

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

In a group, c/b < c/a.

Русский

В группе, c/b < c/a.

LaTeX

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

Lean4

@[to_additive (attr := gcongr) sub_lt_sub_left]
theorem div_lt_div_left' (h : a < b) (c : α) : c / b < c / a :=
  (div_lt_div_iff_left c).2 h

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

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

Разделы

Аффилиация

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