mul_inv_lt_of_lt_mul₀

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_inv_lt_of_lt_mul₀ (h : a < b * c) : a * c⁻¹ < b :=
  by
  contrapose! h
  simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le' zero_le' h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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