mathlib
b173925a - refactor(data/fin): use `order_embedding` for many maps (#5251)

Commit

5 years ago

refactor(data/fin): use `order_embedding` for many maps (#5251) Also swap `data.fin` with `order.rel_iso` in the import tree.

Author

urkud

Parents