English
Renaming induces an isomorphism between the symmetric subalgebras corresponding to σ and τ via an equivalence e: σ ≃ τ.
Русский
Переименование задаёт изоморфизм между симметрическими подалгебрами σ и τ через эквивалентность e: σ ≃ τ.
LaTeX
$$renameSymmetricSubalgebra e : symmetricSubalgebra σ R ≃ₐ[R] symmetricSubalgebra τ R$$
Lean4
/-- `MvPolynomial.rename` induces an isomorphism between the symmetric subalgebras. -/
@[simps!]
def renameSymmetricSubalgebra [CommSemiring R] (e : σ ≃ τ) : symmetricSubalgebra σ R ≃ₐ[R] symmetricSubalgebra τ R :=
AlgEquiv.ofAlgHom (((rename e).comp (symmetricSubalgebra σ R).val).codRestrict _ <| fun x => x.2.rename e)
(((rename e.symm).comp <| Subalgebra.val _).codRestrict _ <| fun x => x.2.rename e.symm)
(AlgHom.ext <| fun p => Subtype.ext <| by simp) (AlgHom.ext <| fun p => Subtype.ext <| by simp)
