Commit 2025-08-26 08:03 b79da6bd

View on Github →

feat(MonoidAlgebra): mapDomain and mapRange as ring homs (#23999) From Toric

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

Modified Mathlib/Algebra/MonoidAlgebra/Lift.lean

added theorem AddMonoidAlgebra.mapRangeRingHom_apply

added theorem AddMonoidAlgebra.mapRangeRingHom_comp

added theorem AddMonoidAlgebra.mapRangeRingHom_id

added theorem AddMonoidAlgebra.mapRangeRingHom_single

added theorem MonoidAlgebra.mapRangeRingHom_apply

added theorem MonoidAlgebra.mapRangeRingHom_comp

added theorem MonoidAlgebra.mapRangeRingHom_id

added theorem MonoidAlgebra.mapRangeRingHom_single

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

modified def AddMonoidAlgebra.mapDomainRingHom

added theorem AddMonoidAlgebra.mapDomainRingHom_comp

added theorem AddMonoidAlgebra.mapDomainRingHom_id

modified theorem AddMonoidAlgebra.mapDomain_mul

modified theorem AddMonoidAlgebra.mapDomain_one

added theorem AddMonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom

modified def MonoidAlgebra.mapDomainRingHom

added theorem MonoidAlgebra.mapDomainRingHom_comp

added theorem MonoidAlgebra.mapDomainRingHom_id

modified theorem MonoidAlgebra.mapDomain_mul

modified theorem MonoidAlgebra.mapDomain_one

added theorem MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom