Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 16:03 a52ce83e

View on Github →

feat(combinatorics/configuration): The order of a projective plane is at least 2 (#11550) This PR proves that the order of a projective plane is strictly larger than 1.

Estimated changes