mathlib3
97843966 - refactor(order/preorder_hom): golf and simp lemmas (#7429)

Commit
4 years ago
refactor(order/preorder_hom): golf and simp lemmas (#7429) The main change here is to adjust `simps` to generate coercion lemmas rather than `.to_fun` for `preorder_hom`, which allows us to auto-generate some simp lemmas. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading