Commit 2022-02-12 19:33 4a4a3a90
View on Github →chore(data/finset/basic): Golf and compress (#11987)
- Move the
lattice
instance earlier so that it can be used to prove lemmas - Golf proofs
- Compress statements within the style guidelines
chore(data/finset/basic): Golf and compress (#11987)
lattice
instance earlier so that it can be used to prove lemmas