English
For indiscrete(1), msymm(μ) equals the sum of all X_i: msymm(Indiscrete(1)) = ∑_i X_i.
Русский
Для indiscrete(1) сумма мономов равна сумме переменных: msymm(Indiscrete(1)) = \\sum_i X_i.
LaTeX
$$$\\mathrm{msymm}_{\\sigma,R}(\\mathrm Nat.Partition.indiscrete(1)) = \\sum_{i\\in \\mathrm{univ}} X_i$$$
Lean4
@[simp]
theorem msymm_one : msymm σ R (.indiscrete 1) = ∑ i, X i :=
by
have : (fun (x : Sym σ 1) ↦ x ∈ Set.univ) = (fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) := by
simp_rw [Set.mem_univ, Nat.Partition.ofSym_one]
symm
rw [Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm) _ (fun s ↦ (s.1.1.map X).prod)]
· apply Fintype.sum_equiv (Equiv.subtypeEquivProp this)
intro x
congr
· intro x
rw [← Multiset.prod_singleton (X x), ← Multiset.map_singleton]
congr
