Commit 2024-02-15 17:35 cfad572b

View on Github →

refactor: drop some *HomClasses (#10544) Drop classes that mix OrderHomClass with algebraic hom classes.

Estimated changes

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

modified def OrderMonoidHomClass.toOrderMonoidHom

modified def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom

Modified Mathlib/Algebra/Order/Hom/Ring.lean