mathlib
4b3198b9 - feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170)

Commit

3 years ago

feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170) If `|P| = |L|`, then `has_lines` and `has_points` are equivalent!

Author

tb65536

Parents

a10cb2f3

mathlib 4b3198b9 - feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170)

mathlib
4b3198b9 - feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170)