coe_basisMonomials — Mathlib

English

The coefficient map of basisMonomials is given by basisMonomials(s) = monomial(s) 1.

Русский

Коэффициентная карта basisMonomials равна monomial s 1.

LaTeX

$$$\\text{basisMonomials}(σ,R) : (Finsupp\\, σ\\, \\mathbb{N}) \\to (\\mathrm{MvPolynomial}(σ,R))$ satisfies $\\text{basisMonomials}(σ,R)(s) = \\mathrm{monomial}(s,1)$$$

Lean4

@[simp]
theorem coe_basisMonomials : (basisMonomials σ R : (σ →₀ ℕ) → MvPolynomial σ R) = fun s => monomial s 1 :=
  rfl

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