one_le_of_le_mul_left₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If PosMulReflectLE α holds and a>0, then a ≤ a·b ⇔ 1 ≤ b.

Русский

Если PosMulReflectLE α справедливо и a>0, тогда a ≤ a·b ⇔ 1 ≤ b.

LaTeX

$$$PosMulReflectLE\,\alpha \land a>0 \Rightarrow (a \le a\cdot b \iff 1 \le b)$$$

Lean4

theorem one_le_of_le_mul_left₀ [PosMulReflectLE α] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b :=
  le_of_mul_le_mul_left (by simpa) ha

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

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

Разделы

Аффилиация

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