constantCoeff_invOfUnit — Mathlib

English

The nth coefficient of invOfUnit φ u (in naturals) satisfies the stated piecewise formula: if n=0 then u^{-1} else -u^{-1} sum over antidiagonal etc.

Русский

n-й коэффициент invOfUnit φ u равен по формуле: если n=0, то u^{-1}, иначе -u^{-1} сумма по антидиагонали и т.д.

LaTeX

$$$ \operatorname{coeff}_n(\operatorname{invOfUnit} φ u) = \begin{cases} ↑u^{-1}, & n = 0 \\ -↑u^{-1} \cdot \sum x \in \operatorname{antidiagonal} n, \; \text{iff } x.2 < n \; \cdot \operatorname{coeff}_{x.1} φ \cdot \operatorname{coeff}_{x.2}(\operatorname{invOfUnit} φ u), & n>0 \end{cases} $$$

Lean4

@[simp]
theorem constantCoeff_invOfUnit (φ : R⟦X⟧) (u : Rˣ) : constantCoeff (invOfUnit φ u) = ↑u⁻¹ := by
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]

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