OAI/Combinatorics/SumProduct/Alignment/AllLevel02.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AllLevelGeometry.cutoff_le_of_subgroup_le line 29
  2. lemma OAI.AllLevelGeometry.top_cutoff_zero line 53
  3. lemma OAI.AllLevelGeometry.cutoff_lt_of_character line 61
  4. lemma OAI.AllLevelGeometry.cutoffs_monotone line 81
  5. lemma OAI.AllLevelGeometry.cutoff_zero line 87
  6. lemma OAI.AllLevelGeometry.cutoff_one line 91
  7. def OAI.AllLevelGeometry.newCutoff line 99
  8. lemma OAI.AllLevelGeometry.newCutoff_le line 102
  9. theorem OAI.AllLevelGeometry.refined_chart line 109
  10. def OAI.AllLevelGeometry.rank line 144
  11. lemma OAI.AllLevelGeometry.rank_strict_drop line 146
  12. lemma OAI.AllLevelGeometry.rank_restrict line 162
  13. def OAI.AllLevelGeometry.comapFiltration line 173
  14. lemma OAI.AllLevelGeometry.restricted_chart line 194
  15. lemma OAI.AllLevelGeometry.restricted_rational line 217
  16. lemma OAI.AllLevelGeometry.restricted_chart_general line 237
  17. lemma OAI.AllLevelGeometry.restricted_rational_general line 258
  18. lemma OAI.AllLevelGeometry.rank_restrict_general line 269
  19. theorem OAI.AllLevelGeometry.restricted_refinement line 281