rename_esymmAlgHom — Mathlib

English

For an equivalence e: σ ≃ τ, renaming preserves msymm: (rename e) (msymm σ R μ) = msymm τ R μ.

Русский

При биекции e: σ ≃ τ сохранение msymm: (rename e)(msymm σ R μ) = msymm τ R μ.

LaTeX

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

Lean4

theorem rename_esymmAlgHom (e : σ ≃ τ) :
    (renameSymmetricSubalgebra e).toAlgHom.comp (esymmAlgHom σ R n) = esymmAlgHom τ R n :=
  by
  ext i : 2
  simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]

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