mathlib
095445ee - refactor(order/*): make `data.set.basic` import `order.bounded_lattice` (#3285)

Commit
5 years ago
refactor(order/*): make `data.set.basic` import `order.bounded_lattice` (#3285) I have two goals: * make it possible to refactor `set` to use `lattice` operations; * make `submonoid.basic` independent of `data.nat.basic`.
Author
Parents
Loading