OAI/Combinatorics/Progressions/Polynomial/DegreeRankLayers.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.rankGenerators line 12
  2. def OAI.Erdos3.NilpotentLieFiltration.rankLayer line 15
  3. theorem OAI.Erdos3.NilpotentLieFiltration.layer_succ_le_rankLayer line 18
  4. theorem OAI.Erdos3.NilpotentLieFiltration.span_rankGenerators_le_rankLayer line 20
  5. theorem OAI.Erdos3.NilpotentLieFiltration.tree_eval_mem_rankLayer line 23
  6. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_le_layer line 27
  7. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_rank_antitone line 33
  8. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_degree_le line 40
  9. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_lex_antitone line 45
  10. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_eq_layer_of_rank_le_one line 51
  11. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_zero line 60
  12. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_one line 63
  13. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_eq_next_of_degree_lt_rank line 66
  14. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_eq_bot_of_degree_gt line 75
  15. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_top_terminal line 81