mul_inv_right_le — Mathlib

English

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

Русский

Если a ≥ 0, то a·b·b⁻¹ ≤ a, равенство при b ≠ 0.

LaTeX

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

Lean4

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

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