le_of_dvd — Mathlib

English

If a divides b and b is nonzero, then a is less than or equal to b.

Русский

Если a делится на b и b ≠ 0, то выполняется a ≤ b.

LaTeX

$$$b \neq 0 \Rightarrow a \mid b \Rightarrow a \le b$$$

Lean4

theorem le_of_dvd : ∀ {a b : Cardinal}, b ≠ 0 → a ∣ b → a ≤ b
  | a, x, b0, ⟨b, hab⟩ => by
    simpa only [hab, mul_one] using
      mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => b0 (by rwa [h, mul_zero] at hab)) a

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