aeval_esymm_eq_multiset_esymm — Mathlib

English

For any algebra homomorphism f: R → S, aeval f(esymm(σ,R,n)) equals esymm(σ,S,n) evaluated with f on the variables: aeval f(esymm(σ,R,n)) = (univ.val.map f).esymm(n).

Русский

Для гомоморфизма алгебр f: R → S выполняется: aeval f(esymm(σ,R,n)) = (univ.val.map f).esymm(n).

LaTeX

$$$ \\operatorname{aeval}_f(\\text{esymm}(\\sigma,R,n)) = (\\mathrm{univ}.val.map f) .\\text{esymm}(n). $$$

Lean4

theorem aeval_esymm_eq_multiset_esymm [Algebra R S] (n : ℕ) (f : σ → S) :
    aeval f (esymm σ R n) = (univ.val.map f).esymm n := by
  simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]

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