Theorems · Definition · commutative algebra

MvPolynomial.esymmAlgHomMonomial

(σ : Type u_1) → {R : Type u_3} → {n : ℕ} → [inst : CommSemiring R] → [Fintype σ] → (Fin n →₀ ℕ) → R → MvPolynomial σ R

The image of a monomial under esymmAlgHom.

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Cited by

9 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFintype