Commit 2025-12-15 15:27 ef1eb32c

View on Github →

feat(Algebra/MonoidAlgebra): complete the map API (#32254) Add congruence isomorphisms in both the ring and monoid arguments. Move mapRangeRingHom from Algebra.MonoidAlgebra.Lift to Algebra.MonoidAlgebra.MapDomain and make its proofs additivisable (by not using lift). Make mapDomainRingHom take a MonoidHom rather than MonoidHomClass.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified def MonoidAlgebra.domCongr

modified theorem MonoidAlgebra.domCongr_apply

modified theorem MonoidAlgebra.domCongr_support

modified theorem MonoidAlgebra.domCongr_toAlgHom

Modified Mathlib/Algebra/MonoidAlgebra/Lift.lean

deleted theorem AddMonoidAlgebra.mapRangeRingHom_apply

deleted theorem AddMonoidAlgebra.mapRangeRingHom_comp

deleted theorem AddMonoidAlgebra.mapRangeRingHom_id

deleted theorem AddMonoidAlgebra.mapRangeRingHom_single

deleted theorem MonoidAlgebra.mapRangeRingHom_apply

deleted theorem MonoidAlgebra.mapRangeRingHom_comp

deleted theorem MonoidAlgebra.mapRangeRingHom_id

deleted theorem MonoidAlgebra.mapRangeRingHom_single

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

added def MonoidAlgebra.mapDomainAddEquiv

added theorem MonoidAlgebra.mapDomainAddEquiv_apply

added theorem MonoidAlgebra.mapDomainAddEquiv_single

added theorem MonoidAlgebra.mapDomainAddEquiv_trans

added def MonoidAlgebra.mapDomainNonUnitalRingHom

added theorem MonoidAlgebra.mapDomainNonUnitalRingHom_comp

added theorem MonoidAlgebra.mapDomainNonUnitalRingHom_id

added def MonoidAlgebra.mapDomainRingEquiv

added theorem MonoidAlgebra.mapDomainRingEquiv_apply

added theorem MonoidAlgebra.mapDomainRingEquiv_single

added theorem MonoidAlgebra.mapDomainRingEquiv_trans

modified def MonoidAlgebra.mapDomainRingHom

modified theorem MonoidAlgebra.mapDomainRingHom_id

added theorem MonoidAlgebra.mapDomain_add

modified theorem MonoidAlgebra.mapDomain_mul

modified theorem MonoidAlgebra.mapDomain_single

modified theorem MonoidAlgebra.mapDomain_sum

added theorem MonoidAlgebra.mapDomain_zero

added def MonoidAlgebra.mapRangeAddEquiv

added theorem MonoidAlgebra.mapRangeAddEquiv_apply

added theorem MonoidAlgebra.mapRangeAddEquiv_single

added theorem MonoidAlgebra.mapRangeAddEquiv_trans

added def MonoidAlgebra.mapRangeRingEquiv

added theorem MonoidAlgebra.mapRangeRingEquiv_apply

added theorem MonoidAlgebra.mapRangeRingEquiv_single

added theorem MonoidAlgebra.mapRangeRingEquiv_trans

added theorem MonoidAlgebra.mapRangeRingHom_apply

added theorem MonoidAlgebra.mapRangeRingHom_comp

added theorem MonoidAlgebra.mapRangeRingHom_id

added theorem MonoidAlgebra.mapRangeRingHom_single

added theorem MonoidAlgebra.symm_mapDomainAddEquiv

added theorem MonoidAlgebra.symm_mapDomainRingEquiv

added theorem MonoidAlgebra.symm_mapRangeAddEquiv

added theorem MonoidAlgebra.symm_mapRangeRingEquiv

added theorem MonoidAlgebra.toRingHom_mapDomainRingEquiv

added theorem MonoidAlgebra.toRingHom_mapRangeRingEquiv

Modified Mathlib/Algebra/Polynomial/Laurent.lean

modified theorem LaurentPolynomial.invert_apply

Modified Mathlib/RingTheory/Polynomial/Opposites.lean