OAI/Combinatorics/Progressions/Polynomial/FreeDegreeRankAdaptedBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.DegreeRankLieFiltration.quotientLie line 14
  2. theorem OAI.Erdos3.DegreeRankLieFiltration.quotientLie_mem line 34
  3. def OAI.Erdos3.DegreeRankLieFiltration.quotientRank line 39
  4. def OAI.Erdos3.FreeDegreeRankLieAlgebra line 51
  5. instance OAI.Erdos3.FreeDegreeRankLieAlgebra.instLieRing line 59
  6. instance OAI.Erdos3.FreeDegreeRankLieAlgebra.instLieAlgebra line 63
  7. def OAI.Erdos3.FreeDegreeRankLieAlgebra.mk line 67
  8. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.mk_surjective line 70
  9. def OAI.Erdos3.FreeDegreeRankLieAlgebra.projection line 72
  10. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.projection_surjective line 75
  11. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.mk_eq_zero line 78
  12. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lowerCentralSeries_eq_bot line 83
  13. def OAI.Erdos3.FreeDegreeRankLieAlgebra.of line 88
  14. def OAI.Erdos3.FreeDegreeRankLieAlgebra.filtration line 91
  15. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.of_mem_layer line 94
  16. instance OAI.Erdos3.FreeDegreeRankLieAlgebra.finite line 102
  17. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.finrank_le line 105
  18. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift_mem_degreeRank line 124
  19. def OAI.Erdos3.FreeDegreeRankLieAlgebra.lift line 136
  20. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_mk line 144
  21. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_projection line 148
  22. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_of line 152
  23. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_mem_layer line 155
  24. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.hom_ext line 160
  25. def OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.canonicalRankGenerators line 183
  26. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.canonicalRankGenerators_span line 188
  27. def OAI.Erdos3.FreeDegreeRankLieAlgebra.layerGenerators line 207
  28. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.layer_eq_span line 211
  29. def OAI.Erdos3.FreeDegreeRankLieAlgebra.layerFamily line 220
  30. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.layerFamily_span line 224
  31. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.layerGenerators_logHeight line 234
  32. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_basis_matrix_logHeight line 287
  33. theorem OAI.Erdos3.exists_bounded_free_degree_rank_model line 343
  34. theorem OAI.Erdos3.exists_adapted_free_degree_rank_model line 485