self_le_mul_right — Mathlib

English

For any a and c with c ≠ 0, a ≤ a*c.

Русский

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

LaTeX

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

Lean4

theorem self_le_mul_right (a : ℕ∞) (hc : c ≠ 0) : a ≤ a * c :=
  by
  obtain rfl | hne := eq_or_ne a ⊤
  · simp [top_mul hc]
  obtain rfl | h0 := eq_or_ne a 0
  · simp
  nth_rewrite 1 [← mul_one a, ENat.mul_le_mul_left_iff h0 hne, ENat.one_le_iff_ne_zero]
  assumption

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