basisMonomials

Mathlib.RingTheory.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.basisMonomials

English

The monomials form a basis on MvPolynomial σ R.

Русский

Мономы образуют базис на MvPolynomial(σ,R).

LaTeX

$$$\\text{basisMonomials}(σ,R) : \\text{Basis} (Finsupp\\, σ\\, \\mathbb{N})\\, R\\, (\\mathrm{MvPolynomial}(σ,R))$$$

Lean4

/-- The monomials form a basis on `MvPolynomial σ R`. -/
def basisMonomials : Basis (σ →₀ ℕ) R (MvPolynomial σ R) :=
  Finsupp.basisSingleOne

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru