mul_inv_lt_iff₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

For a > 0, a^{-1} < b is equivalent to 1 < b a.

Русский

Для a > 0, a^{-1} < b эквивалентно 1 < b a.

LaTeX

$$$0 < a \Rightarrow a^{-1} < b \iff 1 < b a$$$

Lean4

/-- See `mul_inv_lt_iff₀'` for a version with multiplication on the other side. -/
theorem mul_inv_lt_iff₀ (hc : 0 < c) : b * c⁻¹ < a ↔ b < a * c := by
  rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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

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

Разделы

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

Аффилиация

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