Commit 2023-08-14 08:13 c14ff12d

View on Github →

feat(Algebra/MonoidAlgebra/Basic): add domCongr (#6567) This is the AlgEquiv version of Finsupp.domLCongr. MvPolynomial.renameEquiv is a special case of this, but it's probably not worth changing the defeqs to redefine it that way.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added def AddMonoidAlgebra.domCongr

added theorem AddMonoidAlgebra.domCongr_apply

added theorem AddMonoidAlgebra.domCongr_refl

added theorem AddMonoidAlgebra.domCongr_single

added theorem AddMonoidAlgebra.domCongr_support

added theorem AddMonoidAlgebra.domCongr_symm

added theorem AddMonoidAlgebra.domCongr_toAlgHom

modified theorem AddMonoidAlgebra.mapDomain_algebraMap

added def MonoidAlgebra.domCongr

added theorem MonoidAlgebra.domCongr_apply

added theorem MonoidAlgebra.domCongr_refl

added theorem MonoidAlgebra.domCongr_single

added theorem MonoidAlgebra.domCongr_support

added theorem MonoidAlgebra.domCongr_symm

added theorem MonoidAlgebra.domCongr_toAlgHom

modified theorem MonoidAlgebra.mapDomain_algebraMap