OAI/Combinatorics/Progressions/Estimates/SharedFreeLowerFactorization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_shared_free_full_orbit_factorization line 44
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_sharedFreeFactorFreezing line 164
3. def OAI.Erdos3.sharedFreeFactorFreezingConstant line 247
4. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_invariant_native_comparison_model line 290
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_uniform_lower_comparison_model line 378
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_lower_factored_family line 461
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_shared_free_lower_factorization line 552