OAI/Combinatorics/Progressions/Nilpotent/FreeNilpotentSourceBounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.freeLieBoundedCoordinates line 13
  2. theorem OAI.Erdos3.freeLieBoundedCoordinates_eq_zero_iff line 18
  3. def OAI.Erdos3.FreeNilpotentLieAlgebra.coordinates line 31
  4. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.coordinates_mk line 36
  5. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.coordinates_injective line 39
  6. instance OAI.Erdos3.FreeNilpotentLieAlgebra.finite line 50
  7. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.finrank_le line 53
  8. theorem OAI.Erdos3.wordTruncation_lie line 71
  9. def OAI.Erdos3.FreeNilpotentLieAlgebra.expansion line 80
  10. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.expansion_mk line 86
  11. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.expansion_coeff line 89
  12. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.expansion_injective line 95
  13. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.expansion_truncated line 101
  14. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.expansion_lie line 106
  15. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.expansion_of line 113
  16. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.mk_tree_eq_zero_of_length_gt line 130
  17. def OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators line 140
  18. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators_span line 145
  19. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators_card_le line 169
  20. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators_coordinate_height line 187
  21. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators_coordinate_integral line 198
  22. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.exists_bounded_tree_basis line 209
  23. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lift_treeGenerator_height line 238
  24. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lift_basis_matrix_height line 248
  25. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lift_basis_matrix_logHeight line 258
  26. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators_lie_or_zero line 287
  27. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.treeGenerators_lie_coordinate_height line 303
  28. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.exists_bounded_structure_basis line 313
  29. theorem OAI.Erdos3.exists_bounded_free_nilpotent_model line 344
  30. theorem OAI.Erdos3.exists_free_nilpotent_source_basis line 412