OAI/Combinatorics/Progressions/Linear/NativeRankBudget.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.RationalFilteredNilmanifold.RankAlphabet line 14
  2. def OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabetWeight line 16
  3. def OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabetVector line 18
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabetWeight_pos line 20
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabetVector_mem line 22
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabet_card_le line 26
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabet_spans_layer line 37
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.rankAlphabet_span_layer line 56
  9. def OAI.Erdos3.RationalFilteredNilmanifold.finiteRankGenerators line 64
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.finiteRankGenerators_span line 69
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.finiteRankGenerators_card_le line 83
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.finiteRankGenerators_height line 113
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_rankLayer_basis_height line 128
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_canonical_rank_basis_budget line 153