monomialOneHom — Mathlib

English

There is a canonical monoid homomorphism monomialOneHom from the multiplicative finsupp to the mv-polynomial algebra, given by s ↦ monomial(s,1).

Русский

Существет канонический гомоморфизм моноида из умножаемого финсаппа в алгебру mv-многочленов, задаваемый отображением s ↦ monomial(s,1).

LaTeX

$$$\text{monomialOneHom} : (\sigma \to_0 \mathbb{N})^{\times} \to_* MvPolynomial(\sigma,R) \quad\text{with}\quad s \mapsto \mathrm{monomial}(s,1)$$$

Lean4

/-- `fun s ↦ monomial s 1` as a homomorphism. -/
def monomialOneHom : Multiplicative (σ →₀ ℕ) →* MvPolynomial σ R :=
  AddMonoidAlgebra.of _ _

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