OAI/Combinatorics/Progressions/Linear/CommonFreeSpanBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.FreeCoordinateFrame line 15
2. def OAI.Erdos3.FreeCoordinateFrame.mono line 35
3. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.of_mem_treeGenerators line 55
4. theorem OAI.Erdos3.FreeCoordinateFrame.generator_height line 63
5. theorem OAI.Erdos3.exists_submodule_basis_of_spanning_logHeight line 72
6. theorem OAI.Erdos3.exists_petalComparisonSpace_basis_logHeight line 101
7. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeSpan line 201
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonFreeSpan_le_coefficientFreeSpan line 204
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentFreeSpan_le_coefficientFreeSpan line 207
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeSpan_le_layer line 210
11. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation_coefficientFreeSpan line 216
12. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realEvaluation_coefficientFreeSpan line 223
13. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.combined_free_sunflower line 231
14. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_combined_free_sunflower line 248
15. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_common_marked_source_basis line 285
16. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_commonFreeSpan_basis line 387
17. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_dependentFreeSpan_basis line 394
18. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coefficientFreeSpan_basis line 401