rename_msymm — Mathlib

English

For any permutation e, rename e applied to msymm equals msymm with the same μ but indexed by the target set: rename e (msymm σ R μ) = msymm τ R μ.

Русский

Для перестановки e верно: переименование e(mSymm(σ,R,μ)) = msymm(τ,R,μ).

LaTeX

$$$\\text{rename}_{e}(\\mathrm{msymm}_{\\sigma,R}(\\mu)) = \\mathrm{msymm}_{\\tau,R}(\\mu)$$$

Lean4

@[simp]
theorem rename_msymm (μ : n.Partition) (e : σ ≃ τ) : rename e (msymm σ R μ) = msymm τ R μ :=
  by
  rw [msymm, map_sum]
  apply Fintype.sum_equiv (Nat.Partition.ofSymShapeEquiv μ e)
  intro
  rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]
  simp

Похожие утверждения