OAI/Combinatorics/Progressions/Dynamics/LieSubalgebraRepresentativeBudget.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rational_matrix_column_mem_denominatorGrid line 10
  2. theorem OAI.Erdos3.rational_matrix_entry_budget line 17
  3. theorem OAI.Erdos3.rational_section_entry_budget line 34
  4. theorem OAI.Erdos3.representativeInclusion_scaledIntegerGrid_subset line 56
  5. theorem OAI.Erdos3.representativeInclusion_matrixDenominator_le_exp line 65
  6. theorem OAI.Erdos3.representativeInclusion_denominator_spec line 76
  7. theorem OAI.Erdos3.representativeInclusion_gridDenominator_le_exp line 87
  8. def OAI.Erdos3.lieSubalgebraRepresentativeHeight line 118
  9. def OAI.Erdos3.lieSubalgebraRepresentativeParameter line 121
  10. theorem OAI.Erdos3.lieSubalgebraRepresentative_bracket_height line 126
  11. theorem OAI.Erdos3.lieSubalgebraRepresentativeHeight_le_exp line 139
  12. theorem OAI.Erdos3.lieSubalgebraRepresentativeParameter_dimension line 145
  13. theorem OAI.Erdos3.lieSubalgebraRepresentativeParameter_pos line 150
  14. theorem OAI.Erdos3.lieSubalgebraRepresentativeHeight_le_exp_parameter line 155
  15. def OAI.Erdos3.lieSubalgebraInclusionDenominator line 164
  16. theorem OAI.Erdos3.lieSubalgebraInclusionDenominator_spec line 168
  17. theorem OAI.Erdos3.lieSubalgebraInclusionDenominator_grid_bound line 181
  18. theorem OAI.Erdos3.lieSubalgebraRepresentativeBudget_spec line 192