OAI/Combinatorics/Progressions/Nilpotent/NativeRankZeroNiltest.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.dropTopMap line 16
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.dropTopMap_mk line 23
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.dropTopMap_surjective line 32
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.dropTopMap_lipschitz line 42
  5. def OAI.Erdos3.RationalFilteredNilmanifold.dropTopRealOrbit line 65
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.dropTopMap_orbit line 70
  7. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.dropTop line 93
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.dropTop_eval line 105
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.dropTop_evalCyclic line 109
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.dropTop_complexity line 113
  11. def OAI.Erdos3.NativeDegreeRankFamily.component line 133
  12. theorem OAI.Erdos3.NativeDegreeRankFamily.component_eval line 142
  13. theorem OAI.Erdos3.NativeDegreeRankFamily.component_evalCyclic line 145
  14. theorem OAI.Erdos3.NativeDegreeRankFamily.component_complexity line 148
  15. theorem OAI.Erdos3.NativeDegreeRankFamily.rankZero_top_eq_bot line 169
  16. def OAI.Erdos3.NativeDegreeRankFamily.lowerComponent line 173
  17. theorem OAI.Erdos3.NativeDegreeRankFamily.lowerComponent_eval line 177
  18. theorem OAI.Erdos3.NativeDegreeRankFamily.lowerComponent_evalCyclic line 181
  19. theorem OAI.Erdos3.NativeDegreeRankFamily.lowerComponent_complexity line 185