inv_mul_left_le — Mathlib

English

If b ≥ 0, then a⁻¹·(a·b) ≤ b, with equality when a ≠ 0.

Русский

Если b ≥ 0, то a⁻¹·(a·b) ≤ b, равенство достигается, если a ≠ 0.

LaTeX

$$$\forall a\,b\; (0 \le b) \Rightarrow a^{-1} \cdot (a \cdot b) \le b \\ \text{and } (a \neq 0 \Rightarrow a^{-1} \cdot (a \cdot b) = b)$$$

Lean4

/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`. -/
theorem inv_mul_left_le (hb : 0 ≤ b) : a⁻¹ * (a * b) ≤ b := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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