Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
rel_hom.to_preorder_hom_coe_fn
Modification history
2021-06-17 17:10
src/order/preorder_hom.lean
refactor(order/preorder_hom): golf and simp lemmas (#7429) …
Deleted
rel_hom.to_preorder_hom_coe_fn
View on Github →
2021-04-08 15:56
src/order/preorder_hom.lean
feat(order/order_iso_nat): add another flavour of well-foundedness for partial orders (#5434)
Added
rel_hom.to_preorder_hom_coe_fn
View on Github →