Theorem OrderHom.one_eq_id

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.one_eq_idView on Github →