mul_div_mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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