div_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem div_mul (a : ℝ≥0∞) (h0 : b ≠ 0 ∨ c ≠ 0) (htop : b ≠ ∞ ∨ c ≠ ∞) : a / b * c = a / (b / c) :=
  by
  simp only [div_eq_mul_inv]
  rw [ENNReal.mul_inv, inv_inv]
  · ring
  · simpa
  · simpa

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