succNthVal — Mathlib

English

A technical equality expressing the polynomial succNthDefiningPoly as a sum of an X^p part, an X part, and a constant part, matching the recursive construction.

Русский

Техническое тождество выражающее многочлен succNthDefiningPoly как сумму части X^p, части X и константной части, согласованной с рекурсивной конструкцией.

LaTeX

$$succNthDefiningPoly(p,n,a1,a2,bs) = X^p C(a1.coeff 0^{p^{n+1}}) - X C(a2.coeff 0^{p^{n+1}}) + C( a1.coeff(n+1) (bs 0^p)^{p^{n+1}} + nthRemainder ... - a2.coeff(n+1) bs 0^{p^{n+1}} - nthRemainder ... )$$

Lean4

/-- This is the `n+1`st coefficient of our solution, projected from `root_exists`. -/
def succNthVal (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : k :=
  Classical.choose (root_exists p n a₁ a₂ bs ha₁ ha₂)

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