init_isPoly — Mathlib

English

For fixed n, the map x ↦ init(n) x is a polynomial function of the coefficients of x.

Русский

Для фиксированного n отображение x ↦ init(n) x является полиномом по коэффициентам x.

LaTeX

$$$$IsPoly_p\big(\lambda x. \operatorname{init}_n x\big).$$$$

Lean4

/-- `WittVector.init n x` is polynomial in the coefficients of `x`. -/
theorem init_isPoly (n : ℕ) : IsPoly p fun _ _ => init n :=
  select_isPoly (P := fun i => i < n)

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