mul_div_mul_right — Mathlib

English

For c ≠ 0 and c ≠ ∞, a*c / (b*c) = a/b in ENNReal.

Русский

Если c ≠ 0 и c ≠ ∞, то a*c/(b*c) = a/b в ENNReal.

LaTeX

$$$c \neq 0 \land c \neq \infty \Rightarrow \dfrac{a c}{b c} = \dfrac{a}{b}$$$

Lean4

protected theorem mul_div_mul_right (a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) : a * c / (b * c) = a / b := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', mul_one]

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