Theorems · Theorem · commutative algebra

Multiset.pow_smul_esymm

∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
  [IsScalarTower S R R] [SMulCommClass S R R] (s : S) (n : ℕ) (m : Multiset R),
  s ^ n • m.esymm n = (Multiset.map (fun x => s • x) m).esymm n

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringMonoidDistribMulActionIsScalarTowerSMulCommClass