Commit 2026-01-17 11:00 ceaccaaa

View on Github →

feat: lemmas about (Add)MonoidAlgebra.mapRangeRingHom (#33436)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap

added theorem MonoidAlgebra.lift_mapRangeRingHom_algebraMap

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

added theorem MonoidAlgebra.coe_mapRangeRingHom