mathlib
f6b728f4
- feat(data/finset/pointwise): `•` and `⊆` (#14968)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(data/finset/pointwise): `•` and `⊆` (#14968) Port `set` lemmas to `finset`. Tag a few more lemmas with `norm_cast`. Add some missing `to_additive` attributes.
Author
YaelDillies
Parents
7c6cd38b
Loading