OAI/Combinatorics/Progressions/Estimates/RationalLieSubalgebra.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rationalLieStructureHeight line 14
  2. theorem OAI.Erdos3.rationalLieStructureHeight_le_exp line 17
  3. theorem OAI.Erdos3.transportedLieConstants_height_uniform line 39
  4. theorem OAI.Erdos3.exists_bounded_lie_embedding_retraction line 51
  5. theorem OAI.Erdos3.exists_bounded_lie_quotient_section line 69
  6. theorem OAI.Erdos3.rationalLieStructureHeight_inverse_budget line 87
  7. def OAI.Erdos3.lieQuotientCoordinateEquiv line 111
  8. theorem OAI.Erdos3.lieQuotientCoordinateEquiv_apply_mk line 119
  9. def OAI.Erdos3.lieQuotientCoordinateBasis line 127
  10. theorem OAI.Erdos3.lieQuotientCoordinateBasis_matrix line 134
  11. theorem OAI.Erdos3.lieQuotientCoordinateEquiv_symm_apply line 147
  12. theorem OAI.Erdos3.coordinate_span_matrix_range line 158
  13. theorem OAI.Erdos3.exists_bounded_lie_quotient_coordinates line 166
  14. theorem OAI.Erdos3.exists_bounded_lie_quotient_with_structure line 187
  15. theorem OAI.Erdos3.exists_bounded_lie_subalgebra_basis line 223
  16. theorem OAI.Erdos3.lie_subalgebra_finrank_le line 240
  17. theorem OAI.Erdos3.lie_lowerCentralSeries_eq_bot_of_injective line 247
  18. theorem OAI.Erdos3.lie_subalgebra_lowerCentralSeries_eq_bot line 256
  19. theorem OAI.Erdos3.exists_lie_subalgebra_basis_exp_height line 261