OAI/Combinatorics/Progressions/Estimates/SquareGradedRelative.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.unitMonomial line 11
  2. theorem OAI.Erdos3.weight_unitMonomial line 13
  3. theorem OAI.Erdos3.unitMonomial_weight line 17
  4. theorem OAI.Erdos3.unitMonomial_injective line 27
  5. theorem OAI.Erdos3.unitMonomial_add line 32
  6. abbrev OAI.Erdos3.NilpotentLieFiltration.AssociatedGraded line 40
  7. def OAI.Erdos3.NilpotentLieFiltration.associatedGradedIndexEquiv line 43
  8. def OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis line 57
  9. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_apply line 60
  10. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_repr line 67
  11. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_bracket line 74
  12. def OAI.Erdos3.NilpotentLieFiltration.associatedGradedFiltration line 83
  13. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedFiltration_layer line 86
  14. def OAI.Erdos3.NilpotentLieFiltration.gradedMonomialLinear line 117
  15. theorem OAI.Erdos3.NilpotentLieFiltration.gradedMonomialLinear_coe line 129
  16. def OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap line 132
  17. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_apply line 135
  18. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_eq_zero_iff line 139
  19. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_ker line 153
  20. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_lie line 159
  21. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_coordinate line 173
  22. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_basis line 185
  23. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_range line 199
  24. def OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer line 226
  25. theorem OAI.Erdos3.NilpotentLieFiltration.mem_gradedRefiltrationLayer line 229
  26. theorem OAI.Erdos3.NilpotentLieFiltration.mem_gradedRefiltrationLayer_iff line 238
  27. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_le line 243
  28. theorem OAI.Erdos3.NilpotentLieFiltration.layer_succ_le_gradedRefiltrationLayer line 247
  29. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_antitone line 255
  30. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_lie_mem line 262
  31. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_terminal line 272
  32. def OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationSubalgebra line 275
  33. def OAI.Erdos3.NilpotentLieFiltration.gradedRefiltration line 280
  34. theorem OAI.Erdos3.NilpotentLieFiltration.mem_gradedRefiltration_layer line 296
  35. def OAI.Erdos3.NilpotentLieFiltration.squareDiagonalLayer line 310
  36. def OAI.Erdos3.NilpotentLieFiltration.squareRelativeLayer line 316
  37. def OAI.Erdos3.NilpotentLieFiltration.squareGradedDiagonalPiece line 326
  38. def OAI.Erdos3.NilpotentLieFiltration.squareGradedRelativePiece line 330
  39. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedDiagonalPiece_eq_zero_iff line 334
  40. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedRelativePiece_eq_zero_iff line 342
  41. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedDiagonalPiece_lie line 350
  42. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedDiagonal_relative_lie line 358
  43. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedRelativePiece_lie_eq_zero line 372
  44. def OAI.Erdos3.NilpotentLieFiltration.squareGradedRelativeGenerators line 398
  45. def OAI.Erdos3.NilpotentLieFiltration.squareGradedRelativeSubmodule line 401
  46. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedRelative_lie_eq_zero line 404
  47. def OAI.Erdos3.NilpotentLieFiltration.squareGradedRelativeSubalgebra line 419
  48. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedRelative_diagonal_lie_mem line 425
  49. theorem OAI.Erdos3.NilpotentLieFiltration.squareGradedPiece_decomposition line 441