mathlib

mathlib copied to clipboard

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.

---

This PR also adds additional variable declarations, and changes some proofs (in ways which aren't just renames and fixes). Please add this to be PR description.

The changes to the proof are just adding casesI nonempty_fintype _, as preconized by the fintype_finite linter.

There's also the anti-golf in the proof of one_lt_order, and a different proof in coloring.color_classes_finite.

This is all just fintype_finite:

• The "anti-golf" is required because the previous proof was creating another metavariable midway that appeared in a fintype instance. Now that I need to promote the finite instance to the fintype one, I cannot afford to leave this metavariable.
• The different proof for coloring.color_classes_finite is because the previous one was calling the fintype V assumption.

bors merge p=3

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests