self_le_mul_left

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.self_le_mul_left

English

For any a and c with c ≠ 0, c*a ≥ a (equivalently a ≤ c*a).

Русский

Для любых a и c, если c ≠ 0, то a ≤ c*a.

LaTeX

$$$$\forall c,a \in \mathbb{N}_\infty,\ c \ne 0 \Rightarrow a \le c \cdot a.$$$$

Lean4

theorem self_le_mul_left (a : ℕ∞) (hc : c ≠ 0) : a ≤ c * a :=
  by
  rw [mul_comm]
  exact ENat.self_le_mul_right a hc

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

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

Разделы

Аффилиация

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