Theorems · Theorem · commutative algebra

MvPolynomial.esymmAlgHomMonomial_single_one

∀ {σ : Type u_1} {R : Type u_3} {n k : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] {i : Fin n},
  MvPolynomial.esymmAlgHomMonomial σ (fun₀ | i => k) 1 = MvPolynomial.esymm σ R (↑i + 1) ^ k

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringFintype