Def OrderHom.Simps.coe

Modification history

2022-12-14 23:02
Mathlib/Order/Hom/Basic.lean
fix: initialize simps for FunLike structures (#1014) …
Added OrderHom.Simps.coeView on Github →