mul_div_mul_comm — Mathlib

English

For a,b,c,d ∈ ENNReal with c ≠ 0 or d ≠ ∞ and c ≠ ∞ or d ≠ 0, we have a*b/(c*d) = (a/c) * (b/d).

Русский

Для a,b,c,d ∈ ENNReal, при условиях c ≠ 0 ∨ d ≠ ∞ и c ≠ ∞ ∨ d ≠ 0, выполняется a b /(c d) = (a/c) (b/d).

LaTeX

$$$$ \forall a,b,c,d \in \mathbb{R}_{\ge 0}^{\infty},\ (c \neq 0 \lor d \neq \infty) \land (c \neq \infty \lor d \neq 0) \Rightarrow \frac{a b}{c d} = \frac{a}{c} \cdot \frac{b}{d}. $$$$

Lean4

protected theorem mul_div_mul_comm (hc : c ≠ 0 ∨ d ≠ ∞) (hd : c ≠ ∞ ∨ d ≠ 0) : a * b / (c * d) = a / c * (b / d) :=
  by
  simp only [div_eq_mul_inv, ENNReal.mul_inv hc hd]
  ring

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