OAI/Combinatorics/Progressions/Polynomial/RaisedDegreeRank.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.DegreeRankLieFiltration.realLayer line 15
  2. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_lex_antitone line 18
  3. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_congr line 21
  4. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_one line 25
  5. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_rank_zero_eq_one line 32
  6. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_overshoot line 35
  7. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_terminal line 38
  8. theorem OAI.Erdos3.DegreeRankLieFiltration.lie_realLayer_le line 45
  9. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_lie_mem line 53
  10. def OAI.Erdos3.DegreeRankLieFiltration.realification line 58
  11. theorem OAI.Erdos3.DegreeRankLieFiltration.realification_associatedDegree line 68
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.realification_subgroup_eq_realificationSubgroup line 71
  13. theorem OAI.Erdos3.DegreeRankLieFiltration.rational_inclusion_mem_realLayer line 78
  14. theorem OAI.Erdos3.DegreeRankLieFiltration.realificationHom_mem_subgroup line 81
  15. theorem OAI.Erdos3.DegreeRankLieFiltration.realLayer_eq_span line 99
  16. theorem OAI.Erdos3.DegreeRankLieFiltration.realification_subgroup_closed line 109
  17. theorem OAI.Erdos3.DegreeRankLieFiltration.realification_subgroup_connected_simplyConnected line 115
  18. theorem OAI.Erdos3.DegreeRankLieFiltration.realification_layer_lattice_closed_discrete line 122
  19. theorem OAI.Erdos3.DegreeRankLieFiltration.realification_layer_lattice_cocompact line 133
  20. structure OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure line 156
  21. def OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.ComplexityLE line 166
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.ComplexityLE.mono line 169
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.real_associated line 172
  24. def OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup line 175
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_zero line 177
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_le_degree line 183
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_lex_antitone line 190
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_commutator_mem line 193
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_terminal line 198
  30. def OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.orbitEquiv line 201
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.orbitEquiv_eval line 206
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_closed line 215
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_connected_simplyConnected line 219
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_lattice_closed_discrete line 223
  35. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.realSubgroup_lattice_cocompact line 230
  36. def OAI.Erdos3.DegreeRankLieFiltration.withRank line 249
  37. def OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.withRank line 267
  38. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.withRank_complexity line 273
  39. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_degree_rank_structure line 289
  40. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStep_rankSubgroup_eq_bot line 331
  41. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_raised_degree_rank_structure line 343
  42. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.raiseStep_rank_vertical line 368