inverseCoeff — Mathlib

English

Recursively defines the sequence of coefficients for the inverse Witt vector to be constructed when the first coefficient is a unit.

Русский

Рекурсивно задаётся последовательность коэффициентов обратного вектора Витта, когда первый коэффициент является единицей.

LaTeX

$$$\text{inverseCoeff}(a,A):\mathbb{N}\to k \,=\, \begin{cases} \uparrow a^{-1}, & 0, \\ \text{succNthValUnits } n\ a\ A\ (\lambda i: \text{inverseCoeff}(a,A) i.{\text{val}}), & n+1. \end{cases}$$$

Lean4

/-- Recursively defines the sequence of coefficients for the inverse to a Witt vector whose first entry
is a unit.
-/
noncomputable def inverseCoeff (a : Units k) (A : 𝕎 k) : ℕ → k
  | 0 => ↑a⁻¹
  | n + 1 => succNthValUnits n a A fun i => inverseCoeff a A i.val

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