OAI/Combinatorics/RamseyFive/Geometry/LinearForm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.LinearPolynomial.exists_linear_form line 18
2. theorem OAI.SharpRamseyFive.LinearPolynomial.exists_hyperplane line 41
3. lemma OAI.SharpRamseyFive.AffineRealization.projective_pair_rank line 66
4. lemma OAI.SharpRamseyFive.AffineRealization.injective_of_ranks line 86
5. theorem OAI.SharpRamseyFive.AffineRealization.exists_projective_realization line 105
6. theorem OAI.SharpRamseyFive.AffineRealization.plane_cap_of_ranks line 121