Def OrderHom.ofClass

Modification history

2026-09-07 13:06
Mathlib/Order/Hom/Basic.lean
chore: standardise names for coercions from morphism classes to morphisms (#43367) …
Added OrderHom.ofClassView on Github →