OAI/Combinatorics/Progressions/Dynamics/TranslationMajorDimensionBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.finrank_eq_dimension line 18
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.geometry_finrank_le line 22
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.geometry_prod_finrank_le line 27
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.geometry_pair_finrank_le line 43
  5. theorem OAI.Erdos3.two_mul_le_translation_major_budget line 63
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.geometry_pair_finrank_le_budget line 72
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.geometry_prod_finrank_le_budget line 84
  8. theorem OAI.Erdos3.PolynomialTranslationLie.card_le_weightedBasisIndex line 102
  9. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationResidueNilmanifold_base_card_le line 110
  10. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationResidueNilmanifold_finrank_le line 115
  11. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationResidueNilmanifold_prod_finrank_le line 120