select_isPoly — Mathlib

English

Instance asserting that select P x is a polynomial function in Witt vector variables, mirroring selectPoly.

Русский

Инстанс, утверждающий, что select P x является полиномиальной функцией по переменным Witt-вектора, аналогично selectPoly.

LaTeX

$$$ IsPoly p (\lambda _ _ x => select P x) $$$

Lean4

instance select_isPoly {P : ℕ → Prop} : IsPoly p fun _ _ x => select P x :=
  by
  use selectPoly P
  rintro R _Rcr x
  funext i
  apply coeff_select

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