mul_div_cancel' — Mathlib

English

For a ≠ 0 and a ≠ ∞, a * (b / a) = b and hence b / a * a = b.

Русский

Для a ≠ 0 и a ≠ ∞, a * (b / a) = b и следовательно b / a * a = b.

LaTeX

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

Lean4

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

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