inv_mul_cancel_left' — Mathlib

English

For all a,b, if a = 0 implies b = 0 and a = ∞ implies b = 0, then a⁻¹ · (a · b) = b.

Русский

Для всех a, b: если a = 0 ⇒ b = 0 и a = ∞ ⇒ b = 0, тогда a⁻¹ · (a · b) = b.

LaTeX

$$a inverse cancels on the left under conditions: (a = 0 ⇒ b = 0) and (a = ∞ ⇒ b = 0) ⟹ a⁻¹ · (a · b) = b$$

Lean4

/-- See `ENNReal.inv_mul_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected theorem inv_mul_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.inv_mul_cancel, *]

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