English
There is a mapRangeAlgEquiv between MonoidAlgebra A M and MonoidAlgebra B M induced by an AlgEquiv A ≃ₐ[R] B.
Русский
Существует отображение-изоморфизм MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M, индуцированное AlgEquiv A ≃ₐ[R] B.
LaTeX
$$$\\mathrm{mapRangeAlgEquiv}\\ M f : MonoidAlgebra A M \\equiv_{\\mathsf{Alg}} MonoidAlgebra B M$$$
Lean4
/-- The algebra isomorphism of monoid algebras induced by an isomorphism of the base algebras. -/
@[to_additive (attr := simps apply) /--
The algebra isomorphism of additive monoid algebras induced by an isomorphism of the base
algebras. -/
]
noncomputable def mapRangeAlgEquiv (f : A ≃ₐ[R] B) : MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M
where
__ := mapRangeAlgHom M f
invFun := mapRangeAlgHom M (f.symm : B →ₐ[R] A)
left_inv _ := by aesop
right_inv _ := by aesop
