mathlib
fa520678 - refactor(order/fixed_points): rewrite using bundled `preorder_hom`s (#9497)

Commit

4 years ago

refactor(order/fixed_points): rewrite using bundled `preorder_hom`s (#9497) This way `fixed_points.complete_lattice` can be an instance.

Author

urkud

Parents