div_div_cancel' — Mathlib

English

Provided a ≠ 0 and a ≠ ∞, we have a / (a / b) = b.

Русский

При условии a ≠ 0 и a ≠ ∞ выполняется a / (a / b) = b.

LaTeX

$$ (a ≠ 0) ∧ (a ≠ ∞) ⇒ \dfrac{a}{a/b} = b $$

Lean4

/-- See `ENNReal.div_div_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected theorem div_div_cancel' (h₀ : a = 0 → b = 0) (h₁ : a = ∞ → b = 0) : a / (a / b) = b :=
  by
  obtain rfl | ha := eq_or_ne a 0
  · simp [h₀]
  obtain rfl | ha' := eq_or_ne a ∞
  · simp [h₁, top_div_of_lt_top]
  rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (Or.inr ha') (Or.inr ha), ENNReal.div_mul_cancel ha ha']

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