mul_inv_cancel_left' — Mathlib

English

For all a,b with a ≠ 0 and a ≠ ∞, a * (a⁻¹ * b) = b.

Русский

Для всех a,b с a ≠ 0 и a ≠ ∞, выполняется a · (a⁻¹ · b) = b.

LaTeX

$$a \neq 0 \land a \neq \infty \Rightarrow a \cdot (a^{-1} \cdot b) = b$$

Lean4

/-- See `ENNReal.mul_inv_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected theorem mul_inv_cancel_left' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a * (a⁻¹ * b) = b :=
  by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp_all
  obtain rfl | ha := eq_or_ne a ⊤
  · simp_all
  · simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

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