div_mul_cancel' — Mathlib

English

Let a,b ∈ ENNReal with a ≠ 0 and a ≠ ∞. Then a * (b / a) = b.

Русский

Пусть a,b ∈ ENNReal и a ≠ 0, a ≠ ∞. Тогда a * (b / a) = b.

LaTeX

$$a \neq 0 \land a \neq \infty \Rightarrow a * (b / a) = b$$

Lean4

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

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