one_lt_of_lt_mul_left₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If 0 ≤ a and a < a·b, then 1 < b (under PosMulReflectLT).

Русский

Если 0 ≤ a и a < a·b, то 1 < b (при PosMulReflectLT).

LaTeX

$$$0 \le a \land a < a\cdot b \Rightarrow 1 < b$$$

Lean4

theorem one_lt_of_lt_mul_left₀ [PosMulReflectLT α] (ha : 0 ≤ a) (h : a < a * b) : 1 < b :=
  lt_of_mul_lt_mul_left (by simpa) ha

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

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

Разделы

Аффилиация

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