basis — Mathlib

English

There is a basis for the subspace of polynomials of degree < n given by the monomials X^i with i < n, indexed by Fin(n).

Русский

Существует базис подпространства многочленов степеней меньше n, состоящий из мономов X^i с i < n, индексированных по Fin(n).

LaTeX

$$$$ \\text{basis}(n) : \\mathrm{Basis}(\\mathrm{Fin}(n), R, R[X]_{n}). $$$$

Lean4

/-- Basis for `R[X]_n` given by `X^i` with `i < n`. -/
noncomputable def basis (n : ℕ) : Basis (Fin n) R R[X]_n :=
  .ofEquivFun (degreeLTEquiv R n)

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