inv_mul_lt_of_lt_mul₀

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#inv_mul_lt_of_lt_mul₀

English

If a < b c in a linear ordered group with zero, then b^{-1} a < c.

Русский

Если a < b c в линейно упорядоченной группе с нулём, то b^{-1} a < c.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\alpha, \\\\ a < b c \\\\Rightarrow b^{-1} a < c$$$

Lean4

theorem inv_mul_lt_of_lt_mul₀ (h : a < b * c) : b⁻¹ * a < c :=
  by
  rw [mul_comm] at *
  exact mul_inv_lt_of_lt_mul₀ h

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

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

Разделы

Аффилиация

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