OAI/Combinatorics/Progressions/Linear/CommonRealDependentProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.coordinateSpace_first line 23
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.coordinateSpace_sparse line 28
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.coordinateSpace_dependent line 35
4. theorem OAI.Erdos3.NativeDegreeRankFamily.nativeCoefficientCoordinates_eq_real line 62
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_dependent_coordinateSpace_eq line 85
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_real_dependent_remainder line 94
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_native_dependent_remainder line 108