mathlib3
26c71658 - refactor(combinatorics/configuration): Refactor `projective_plane` to extend `has_points` and `has_lines` (#18436)

Commit
2 years ago
refactor(combinatorics/configuration): Refactor `projective_plane` to extend `has_points` and `has_lines` (#18436) This PR refactors `projective_plane` to extend `has_points` and `has_lines`. For this to work in Lean3, we need to use `old_structure_cmd`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading