OAI/Combinatorics/RamseyFive/Geometry/FinrankSpanImage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.ScalarExtension.finrank_span_image line 17
2. lemma OAI.SharpRamseyFive.AffineChart.span_lift_normalize line 30
3. lemma OAI.SharpRamseyFive.AffineChart.finrank_lift_normalize line 42
4. lemma OAI.SharpRamseyFive.AffineChart.lift_mem_span_pair line 50
5. theorem OAI.SharpRamseyFive.ProjectiveReduction.exists_to_four line 75
6. lemma OAI.SharpRamseyFive.ProjectiveReduction.nonzero_of_rank_preserved line 90
7. theorem OAI.SharpRamseyFive.AffineRealization.exists_realization line 110
8. theorem OAI.SharpRamseyFive.SubspaceExtension.exists_add_rank line 150
9. theorem OAI.SharpRamseyFive.SubspaceExtension.exists_rank line 171