OAI/Combinatorics/Progressions/Estimates/NativeSharedFreeFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coefficient_bases line 24
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_controlled_coefficient_bases line 32
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_native_common_free_model line 61
4. theorem OAI.Erdos3.exists_native_shared_common_factorization line 153
5. theorem OAI.Erdos3.exists_native_shared_free_family line 317