English
In the ring of multivariate power series, the inverse of a product is the product of the inverses in reverse order: (φ ψ)⁻¹ = ψ⁻¹ φ⁻¹.
Русский
В кольце многовариантных формальных рядов обратное произведение равно произведению обратных в обратном порядке: (φ ψ)⁻¹ = ψ⁻¹ φ⁻¹.
LaTeX
$$$(\phi \psi)^{-1} = \psi^{-1} \phi^{-1}$$$
Lean4
@[simp]
protected theorem mul_inv_rev (φ ψ : MvPowerSeries σ k) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
by
by_cases h : constantCoeff (φ * ψ) = 0
· rw [inv_eq_zero.mpr h]
simp only [map_mul, mul_eq_zero] at h
rcases h with h | h <;> simp [inv_eq_zero.mpr h]
· rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]
simp only [not_or, map_mul, mul_eq_zero] at h
rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
MvPowerSeries.inv_mul_cancel _ h.right]
