English
This defines the nth coefficient of the inverse Witt vector when the first entry is a unit; it is given by a factor involving a^{-1} to a p-power, the next coefficient of A, and a remainder term.
Русский
Это определение n-го коэффициента обратного вектора Витта, когда первая запись является единицей; коэффициент задаётся через a^{-1}^{p^{n+1}}, следующую коэффициенту A и остаток nthRemainder.
LaTeX
$$$\text{succNthValUnits}(n,a,A,bs) = -\uparrow(a^{-1}^{p^{n+1}}) \cdot ( A_{n+1} \cdot a^{-1^{p^{n+1}}} + \nthRemainder\ p\ n\ (\mathrm{truncateFun}\ (n+1)\ A)\ bs )$$$
Lean4
/-- This is the `n+1`st coefficient of our inverse. -/
def succNthValUnits (n : ℕ) (a : Units k) (A : 𝕎 k) (bs : Fin (n + 1) → k) : k :=
-↑(a⁻¹ ^ p ^ (n + 1)) * (A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) bs)
