Commit 2024-09-12 06:16 06a043ee

View on Github →

feat(Combinatorics/Configuration): Projective planes over fields (#16684) This PR constructs projective planes over fields (in particular, finite projective planes).

Estimated changes

Modified Mathlib/Combinatorics/Configuration.lean

added theorem Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero

added theorem Configuration.ofField.eq_or_eq_of_orthogonal

added theorem Configuration.ofField.mem_iff

Modified Mathlib/Data/Matrix/Rank.lean

added theorem LinearIndependent.rank_matrix

added theorem Matrix.rank_add_rank_le_card_of_mul_eq_zero