one_le_of_le_mul_left

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

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

← MathLib Explorer

English

If a·b ≤ b, then 1 ≤ a.

Русский

Если a·b ≤ b, то 1 ≤ a.

LaTeX

$$$ a \\cdot b \\le b \\rightarrow 1 \\le a $$$

Lean4

@[to_additive]
theorem one_le_of_le_mul_left [MulRightReflectLE α] {a b : α} (h : b ≤ a * b) : 1 ≤ a :=
  le_of_mul_le_mul_right' (a := b) <| by simpa only [one_mul]

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

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

Разделы

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

Аффилиация

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