English
Let S be a monoid acting on R via a distributive action, and let n ∈ N. For s ∈ S and m ∈ Multiset R, s^n • m.esymm n equals (m.map (s • ·)).esymm n.
Русский
Пусть S — моноид действует на R, и n ∈ N. Тогда для s ∈ S и m ∈ Multiset R верно: s^n • esymm_n(m) = esymm_n(m.map (s • ·)).
LaTeX
$$s^n • m.esymm n = (m.map (s • \cdot)).esymm n$$
Lean4
theorem pow_smul_esymm {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] [SMulCommClass S R R] (s : S)
(n : ℕ) (m : Multiset R) : s ^ n • m.esymm n = (m.map (s • ·)).esymm n :=
by
rw [esymm, smul_sum, map_map]
trans ((powersetCard n m).map (fun x : Multiset R ↦ s ^ card x • x.prod)).sum
· refine congr_arg _ (map_congr rfl (fun x hx ↦ ?_))
rw [Function.comp_apply, (mem_powersetCard.1 hx).2]
·
simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]
-- TODO: `Multiset.insert_eq_cons` being simp means that `esymm {x, y}` is not simp normal form
