OAI/Combinatorics/Progressions/Geometry/RealFastCoefficientCoordinates.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.extendInitialCoordinates line 17
  2. theorem OAI.Erdos3.extendInitialCoordinates_castLE line 22
  3. def OAI.Erdos3.initialHorizontalEquiv line 26
  4. theorem OAI.Erdos3.initialHorizontalEquiv_symm_projection line 58
  5. theorem OAI.Erdos3.initialHorizontalEquiv_projection line 70
  6. theorem OAI.Erdos3.realDenominatorGrid_single line 88
  7. theorem OAI.Erdos3.extendInitialCoordinates_grid line 96
  8. theorem OAI.Erdos3.norm_extendInitialCoordinates_le line 108
  9. theorem OAI.Erdos3.norm_extendInitialCoordinates line 117
  10. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal_projector_repr line 139
  11. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal_projector line 155
  12. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal_eq_zero_iff line 164
  13. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRealEquiv_coordinates line 200
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_projector_repr line 238
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_projector line 255
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_eq_zero_iff line 264
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontal_projector line 310
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontal_projector_repr line 323
  19. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontalEquiv line 332
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontalEquiv_projection line 343
  21. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRealEquiv_basis line 369
  22. def OAI.Erdos3.NilpotentLieFiltration.fastCoefficientRealEquiv line 383
  23. theorem OAI.Erdos3.NilpotentLieFiltration.fastCoefficientRealEquiv_mk line 389
  24. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientBasis line 395
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientBasis_repr_basis line 401
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientBasis_matrix line 414
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientBasis_symm line 428