OAI/Combinatorics/Progressions/Estimates/OptionMarkedSurjective.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.optionFiltrations line 20
  2. theorem OAI.Erdos3.NilpotentLieFiltration.optionFiltrations_none line 26
  3. theorem OAI.Erdos3.NilpotentLieFiltration.optionFiltrations_some line 29
  4. def OAI.Erdos3.optionMarkedComponents line 35
  5. def OAI.Erdos3.optionMarkedLieMap line 41
  6. theorem OAI.Erdos3.optionMarkedLieMap_none line 46
  7. theorem OAI.Erdos3.optionMarkedLieMap_some line 50
  8. theorem OAI.Erdos3.realification_optionMarkedLieMap_none line 54
  9. theorem OAI.Erdos3.realification_optionMarkedLieMap_some line 65
  10. theorem OAI.Erdos3.optionMarkedLieMap_mem_layer line 75
  11. theorem OAI.Erdos3.realBCHPiEquiv_optionMarkedLieMap_none line 90
  12. theorem OAI.Erdos3.realBCHPiEquiv_optionMarkedLieMap_some line 105
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionMarkedLieMap_native_logHeight line 140
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionMarkedLieMap_native_logHeight_max line 177
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionMarkedLieMap_native_matrix_height line 184
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionMarkedLieMap_piRealOrbit_log line 205
  17. theorem OAI.Erdos3.optionMarkedLieMap_surjective line 264
  18. theorem OAI.Erdos3.quotientInducedMark_surjective line 278
  19. theorem OAI.Erdos3.optionQuotientMarkedLieMap_surjective line 286