Commit 2025-02-04 15:53 abba7259

View on Github →

chore: split mapDomain out of MonoidAlgebra.Defs (#21398) This is not the most inspired split, but it gets MonoidAlgebra.Defs below the longFile limit. If this provokes someone into working out how to do a better split, that's wonderful. :-)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

deleted def AddMonoidAlgebra.mapDomainRingHom

deleted theorem AddMonoidAlgebra.mapDomain_mul

deleted theorem AddMonoidAlgebra.mapDomain_one

deleted theorem AddMonoidAlgebra.mapDomain_single

deleted theorem AddMonoidAlgebra.mapDomain_sum

deleted def MonoidAlgebra.mapDomainRingHom

deleted theorem MonoidAlgebra.mapDomain_mul

deleted theorem MonoidAlgebra.mapDomain_one

deleted theorem MonoidAlgebra.mapDomain_sum

Modified Mathlib/Algebra/MonoidAlgebra/Ideal.lean

Created Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

added def AddMonoidAlgebra.mapDomainRingHom

added theorem AddMonoidAlgebra.mapDomain_mul

added theorem AddMonoidAlgebra.mapDomain_one

added theorem AddMonoidAlgebra.mapDomain_single

added theorem AddMonoidAlgebra.mapDomain_sum

added def MonoidAlgebra.mapDomainRingHom

added theorem MonoidAlgebra.mapDomain_mul

added theorem MonoidAlgebra.mapDomain_one

added theorem MonoidAlgebra.mapDomain_sum

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean