OAI/Combinatorics/RamseyFive/Geometry/AmbientPivotPotential.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.ProjectiveIncidence.projective_card_pos_of_fiveline 14 - lemma
OAI.SharpRamseyFive.ProjectiveIncidence.ambient_pivotPotentialline 21