OAI/Combinatorics/Progressions/Nilpotent/DegreeRankBCH.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.DegreeRankLieFiltration.layerIdeal line 12
  2. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_layerIdeal line 19
  3. abbrev OAI.Erdos3.DegreeRankLieFiltration.Group line 22
  4. def OAI.Erdos3.DegreeRankLieFiltration.subgroup line 24
  5. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_subgroup line 27
  6. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_normal line 30
  7. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_lex_antitone line 33
  8. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_zero line 36
  9. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_one line 40
  10. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_le_associatedDegree line 45
  11. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_commutator_mem line 48
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_eq_bot_of_past_top line 53
  13. theorem OAI.Erdos3.DegreeRankLieFiltration.subgroup_terminal line 63