inv_mul_cancel_right' — Mathlib

English

For all a,b with b ≠ 0 and b ≠ ∞, a · b⁻¹ · b = a.

Русский

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

LaTeX

$$b = 0 \rightarrow a = 0 \and b = \infty \rightarrow a = 0 \Rightarrow a \cdot b^{-1} \cdot b = a$$

Lean4

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

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