mul_div_cancel_right' — Mathlib

English

For a,b with a ≠ 0 and a ≠ ∞, a · (b / a) = b.

Русский

Для a,b при a ≠ 0 и a ≠ ∞ выполняется a · (b / a) = b.

LaTeX

$$a \neq 0 \rightarrow a \cdot (b / a) = b \quad \text{(under appropriate conditions)}$$

Lean4

/-- See `ENNReal.mul_div_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`. -/
protected theorem mul_div_cancel_right' (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : a * b / b = a :=
  ENNReal.mul_inv_cancel_right' hb₀ hb

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