selectPoly — Mathlib

English

For any P, the coefficient of x under select P is the evaluation of x.coeff under the polynomial selectPoly P at that index.

Русский

Для любого P коэффициент (select P x) равен вычислению x.coeff по полиному selectPoly P на этом индексе.

LaTeX

$$$ (select P x).coeff n = aeval x.coeff (selectPoly P n) $$$

Lean4

/-- The polynomial that witnesses that `WittVector.select` is a polynomial function.
`selectPoly n` is `X n` if `P n` holds, and `0` otherwise. -/
def selectPoly (n : ℕ) : MvPolynomial ℕ ℤ :=
  if P n then X n else 0

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