Commit 2025-09-08 14:22 3a09953b

View on Github →

feat(MonoidAlgebra): mapRange as an AlgHom (#28956) From Toric

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem AddMonoidAlgebra.coe_liftNCAlgHom

modified def AddMonoidAlgebra.lift

modified def MonoidAlgebra.GroupSMul.linearMap

modified theorem MonoidAlgebra.GroupSMul.linearMap_apply

added theorem MonoidAlgebra.coe_liftNCAlgHom

added theorem MonoidAlgebra.mapDomainRingHom_comp_algebraMap

added theorem MonoidAlgebra.mapRangeAlgHom_apply

added theorem MonoidAlgebra.mapRangeAlgHom_single

added theorem MonoidAlgebra.mapRangeRingHom_comp_algebraMap

added theorem MonoidAlgebra.toRingHom_mapRangeAlgHom