instInv — Mathlib

English

The coefficient of φ⁻¹ at n is given by the recursive formula: coeff n φ⁻¹ = if n = 0 then (constantCoeff φ)⁻¹ else -(constantCoeff φ)⁻¹ · ∑_{x ∈ antidiagonal n} (coeff x.1 φ) · (coeff x.2 φ⁻¹).

Русский

Коэффициент φ⁻¹ в позиции n задаётся рекурсивной формулой: coeff n φ⁻¹ = если n = 0, то (constantCoeff φ)⁻¹, иначе -(constantCoeff φ)⁻¹ · ∑_{x ∈ antidiagonal n} coeff x.1 φ · coeff x.2 φ⁻¹.

LaTeX

$$$ coeff\ n\ (\varphi^{-1}) = \begin{cases} (constantCoeff\ \varphi)^{-1}, & n = 0 \\ -(constantCoeff\ \varphi)^{-1} \cdot \sum_{x \in antidiagonal\ n} coeff x.1\varphi \cdot coeff x.2 (\varphi^{-1}), & \text{иначе} \end{cases}$$$

Lean4

instance : Inv (MvPowerSeries σ k) :=
  ⟨MvPowerSeries.inv⟩

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