basisMonomials — Mathlib

English

The monomials X^n (n ∈ N) form a basis of the polynomial ring R[X] over R; as an R-module, R[X] is freely generated by the monomials.

Русский

Мономы X^n (n ∈ N) образуют базис кольца многочленов над R; как модуль над R, R[X] свободно порождается мономами.

LaTeX

$$basisMonomials is a Basis ℕ R R[X]$$

Lean4

/-- The monomials form a basis on `R[X]`. To get the rank of a polynomial ring,
use this and `Basis.mk_eq_rank`. -/
def basisMonomials : Basis ℕ R R[X] :=
  Basis.ofRepr (toFinsuppIsoLinear R)

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