mathlib
1e6b748c
- chore(combinatorics/*): Fix lint (#16031)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(combinatorics/*): Fix lint (#16031) Fix the linting errors coming from `fintype_finite`, `to_additive_doc` and `doc_blame`. Pull out a `[projective_plane P L]` assumption to a `variables` declaration in `combinatorics.configuration`.
Author
YaelDillies
Parents
1ec48762
Loading