Theorem OrderHom.mul_eq_comp

Modification history

2026-06-23 15:06
Mathlib/Algebra/Order/Group/End.lean
feat: `Monoid` and `Group` instances for `OrderHom` and `OrderIso` (#40515) …
Added OrderHom.mul_eq_compView on Github →