Commit 2026-03-21 17:40 8d6c9efb

View on Github →

feat(Algebra/MonoidAlgebra): map and comapDomain (#36768) This follows what we have for Finsupp and Polynomial.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

deleted theorem AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap

added theorem AddMonoidAlgebra.lift_mapRingHom_algebraMap

modified theorem MonoidAlgebra.algebraMap_def

deleted theorem MonoidAlgebra.lift_mapRangeRingHom_algebraMap

added theorem MonoidAlgebra.lift_mapRingHom_algebraMap

added theorem MonoidAlgebra.mapAlgHom_apply

added theorem MonoidAlgebra.mapAlgHom_single

deleted theorem MonoidAlgebra.mapRangeAlgHom_apply

deleted theorem MonoidAlgebra.mapRangeAlgHom_single

deleted theorem MonoidAlgebra.mapRangeRingHom_comp_algebraMap

added theorem MonoidAlgebra.mapRingHom_comp_algebraMap

added theorem MonoidAlgebra.symm_mapAlgEquiv

deleted theorem MonoidAlgebra.symm_mapRangeAlgEquiv

added theorem MonoidAlgebra.toRingHom_mapAlgHom

deleted theorem MonoidAlgebra.toRingHom_mapRangeAlgHom

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

deleted theorem MonoidAlgebra.coe_mapRangeRingHom

added theorem MonoidAlgebra.coe_mapRingHom

added theorem MonoidAlgebra.coeff_comapDomain

added theorem MonoidAlgebra.coeff_map

added def MonoidAlgebra.comapDomain

added def MonoidAlgebra.comapDomainAddMonoidHom

added theorem MonoidAlgebra.comapDomain_add

added theorem MonoidAlgebra.comapDomain_single_map

added theorem MonoidAlgebra.comapDomain_single_of_not_mem_range

added theorem MonoidAlgebra.comapDomain_zero

added def MonoidAlgebra.map

added def MonoidAlgebra.mapAddEquiv

added theorem MonoidAlgebra.mapAddEquiv_apply

added theorem MonoidAlgebra.mapAddEquiv_single

added theorem MonoidAlgebra.mapAddEquiv_trans

added theorem MonoidAlgebra.mapDomain_comapDomain

deleted def MonoidAlgebra.mapRangeAddEquiv

deleted theorem MonoidAlgebra.mapRangeAddEquiv_apply

deleted theorem MonoidAlgebra.mapRangeAddEquiv_single

deleted theorem MonoidAlgebra.mapRangeAddEquiv_trans

deleted def MonoidAlgebra.mapRangeRingEquiv

deleted theorem MonoidAlgebra.mapRangeRingEquiv_apply

deleted theorem MonoidAlgebra.mapRangeRingEquiv_single

deleted theorem MonoidAlgebra.mapRangeRingEquiv_trans

deleted theorem MonoidAlgebra.mapRangeRingHom_apply

deleted theorem MonoidAlgebra.mapRangeRingHom_comp

deleted theorem MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom

deleted theorem MonoidAlgebra.mapRangeRingHom_id

deleted theorem MonoidAlgebra.mapRangeRingHom_single

added def MonoidAlgebra.mapRingEquiv

added theorem MonoidAlgebra.mapRingEquiv_apply

added theorem MonoidAlgebra.mapRingEquiv_single

added theorem MonoidAlgebra.mapRingEquiv_trans

added theorem MonoidAlgebra.mapRingHom_apply

added theorem MonoidAlgebra.mapRingHom_comp

added theorem MonoidAlgebra.mapRingHom_comp_mapDomainRingHom

added theorem MonoidAlgebra.mapRingHom_id

added theorem MonoidAlgebra.mapRingHom_single

added theorem MonoidAlgebra.map_id

added theorem MonoidAlgebra.map_map

added theorem MonoidAlgebra.map_neg

added theorem MonoidAlgebra.map_single

added theorem MonoidAlgebra.map_sub

added theorem MonoidAlgebra.ofCoeff_mapRange

added theorem MonoidAlgebra.symm_mapAddEquiv

deleted theorem MonoidAlgebra.symm_mapRangeAddEquiv

deleted theorem MonoidAlgebra.symm_mapRangeRingEquiv

added theorem MonoidAlgebra.symm_mapRingEquiv

deleted theorem MonoidAlgebra.toRingHom_mapRangeRingEquiv

added theorem MonoidAlgebra.toRingHom_mapRingEquiv

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.comapDomain_single_of_not_mem_range

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

modified def IsAdjoinRootMonic.basis

Modified Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean