OAI/Combinatorics/Progressions/Estimates/RealifiedTopQuotient.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.lieQuotientProjection line 13
  2. theorem OAI.Erdos3.lieQuotientProjection_mk line 19
  3. def OAI.Erdos3.lieQuotientFiberProduct line 23
  4. def OAI.Erdos3.lieQuotientFiberMap line 39
  5. theorem OAI.Erdos3.lieQuotientFiberMap_bijective line 49
  6. def OAI.Erdos3.lieQuotientFiberEquiv line 78
  7. theorem OAI.Erdos3.lieQuotientFiberEquiv_apply line 86
  8. theorem OAI.Erdos3.NilpotentLieFiltration.mem_layer_iff_quotient_and_projection line 100
  9. def OAI.Erdos3.NilpotentLieFiltration.quotientFiberEquiv line 130
  10. theorem OAI.Erdos3.NilpotentLieFiltration.quotientFiberEquiv_layer_surjective line 136
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_quotient_marked_layer_lift line 168
  12. theorem OAI.Erdos3.NilpotentLieFiltration.quotientFiberMap_layer_surjective line 203
  13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_adapted_quotient_fiber_polynomial_lift line 229
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_quotient_fiber_polynomialOrbit_lift line 289
  15. def OAI.Erdos3.quotientInducedMapHeightBudget line 318
  16. theorem OAI.Erdos3.exists_quotientInducedMapHeightBudget_power line 322
  17. theorem OAI.Erdos3.lieQuotientProjection_basis_logHeight line 330
  18. def OAI.Erdos3.quotientInducedMarkHeightBudget line 388
  19. theorem OAI.Erdos3.quotientInducedMark_basis_logHeight line 391
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientInducedMark_native_logHeight line 438
  21. def OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientHom line 472
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientHom_mk line 479
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientHom_bijective line 483
  24. def OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientEquiv line 501
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientEquiv_mk line 506
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientEquiv_mem_layer_iff line 510
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realificationTopQuotientEquiv_projection line 524