OAI/Combinatorics/Progressions/Linear/SquareBasisGeometry.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.squareCoordinates line 19
  2. def OAI.Erdos3.NilpotentLieFiltration.squareBasis line 39
  3. theorem OAI.Erdos3.NilpotentLieFiltration.squareBasis_inl line 43
  4. theorem OAI.Erdos3.NilpotentLieFiltration.squareBasis_inr line 47
  5. theorem OAI.Erdos3.NilpotentLieFiltration.squareBasis_repr_inl line 51
  6. theorem OAI.Erdos3.NilpotentLieFiltration.squareBasis_repr_inr line 56
  7. theorem OAI.Erdos3.NilpotentLieFiltration.mem_squareLayer_iff_second_and_difference line 75
  8. def OAI.Erdos3.NilpotentLieFiltration.adaptedSquareBasis line 84
  9. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedSquareBasis_inl line 89
  10. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedSquareBasis_inr line 94
  11. def OAI.Erdos3.NilpotentLieFiltration.squareBasisWeight line 102
  12. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedSquareBasis_layers line 105
  13. abbrev OAI.Erdos3.NilpotentLieFiltration.QuotientTopBasisIndex line 158
  14. def OAI.Erdos3.NilpotentLieFiltration.quotientTopBasis line 163
  15. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopBasis_apply line 167
  16. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopBasis_repr_mk line 171
  17. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopBasis_layers line 175
  18. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd line 192
  19. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonal line 200
  20. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd_mk line 209
  21. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonal_mk line 213
  22. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd_diagonal line 217
  23. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd_mem line 222
  24. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonal_mem line 229
  25. def OAI.Erdos3.NilpotentLieFiltration.squarePairMap line 249
  26. theorem OAI.Erdos3.NilpotentLieFiltration.squarePairMap_false line 252
  27. theorem OAI.Erdos3.NilpotentLieFiltration.squarePairMap_true line 253
  28. theorem OAI.Erdos3.NilpotentLieFiltration.squarePairMap_injective line 255
  29. theorem OAI.Erdos3.NilpotentLieFiltration.squareLattice_eq_pair_comap line 260
  30. theorem OAI.Erdos3.NilpotentLieFiltration.card_squareBasis_index_le line 277
  31. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedSquareBasis_pairMap_height line 285
  32. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndPolynomialMap line 316
  33. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonalPolynomialMap line 322
  34. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolMap line 328
  35. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonalSymbolMap line 333
  36. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolMap_symbol line 338
  37. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonalSymbolMap_symbol line 343
  38. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndPolynomialMap_diagonal line 347
  39. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolMap_diagonal line 356
  40. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndPolynomialMap_quotient line 362
  41. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonalPolynomialMap_quotient line 376
  42. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolMap_quotient line 390
  43. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonalSymbolMap_quotient line 398
  44. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolMap_surjective line 406
  45. abbrev OAI.Erdos3.NilpotentLieFiltration.ReducedSquareBasisIndex line 421
  46. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareBasis line 427
  47. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareBasis_layers line 433
  48. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd_basis_height line 439
  49. abbrev OAI.Erdos3.NilpotentLieFiltration.QuotientTopSymbolIndex line 468
  50. abbrev OAI.Erdos3.NilpotentLieFiltration.ReducedSquareSymbolIndex line 471
  51. def OAI.Erdos3.NilpotentLieFiltration.quotientTopSymbolBasis line 477
  52. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolBasis line 482
  53. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolMap_basis_height line 487
  54. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolMap_monomial_blocks line 498
  55. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedSquareBasis_structure_bound line 522
  56. theorem OAI.Erdos3.NilpotentLieFiltration.exists_adaptedSquareBasis_grid line 549