A monomial as a product of variables

Multiplying together a multiset of variables, one factor per element, gives the monomial whose exponent vector is the multiplicity function of the multiset: TauCeti.prod_map_X_eq_monomial. Mathlib's MvPolynomial.prod_X_pow_eq_monomial says the same thing for a product indexed by the support of an exponent vector; this is the multiset-indexed form, which is how the monomials of MvPolynomial.hsymm and MvPolynomial.msymm are written.

Main results

• TauCeti.prod_map_X_eq_monomial: the product of a multiset of variables is the monomial with coefficient 1 at the multiplicity function of the multiset.

theorem TauCeti.prod_map_X_eq_monomial {σ : Type u_1} [DecidableEq σ] {R : Type u_2} [CommSemiring R] (s : Multiset σ) : (Multiset.map MvPolynomial.X s).prod = (MvPolynomial.monomial (Multiset.toFinsupp s)) 1

A monomial is the product of the variables it uses, with multiplicity. This is the form in which the monomials of MvPolynomial.hsymm and MvPolynomial.msymm are written.