mathlib
ad3a37c5 - chore(order/complete_lattice): don't import data.nat.order

Commit

3 years ago

chore(order/complete_lattice): don't import data.nat.order

References

complete_lattice_imports

Author

kim-em

kim-em

Parents

Loading