Commit 2023-12-16 07:33 5e43fdc9

View on Github →

feat(Algebra/Module/Basic): add RingHom.smulOneHom (#9064) This also renames the existing smulOneHom to MonoidHom.smulOneHom.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem RingHom.smulOneHom_eq_algebraMap

Modified Mathlib/Algebra/Module/Basic.lean

added def RingHom.smulOneHom

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added def MonoidHom.smulOneHom

deleted def smulOneHom