le_mul_left

Mathlib.SetTheory.Cardinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.le_mul_left

English

If b ≠ 0, then a ≤ b · a.

Русский

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

LaTeX

$$$$(b \neq 0) \Rightarrow a \le b \cdot a$$$$

Lean4

theorem le_mul_left {a b : Cardinal} (h : b ≠ 0) : a ≤ b * a :=
  by
  convert mul_le_mul_right' (one_le_iff_ne_zero.mpr h) a
  rw [one_mul]

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

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

Разделы

Аффилиация

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