OAI/Combinatorics/Progressions/Linear/RationalTagConstraintChartBasis.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.realSubmoduleBasis line 23
  2. theorem OAI.Erdos3.realSubmoduleBasis_coe line 26
  3. def OAI.Erdos3.realSubmoduleParameterization line 32
  4. theorem OAI.Erdos3.realSubmoduleParameterization_basis line 35
  5. theorem OAI.Erdos3.exists_rational_matrix_of_grid_columns line 51
  6. theorem OAI.Erdos3.basis_projection_range_eq_span line 59
  7. theorem OAI.Erdos3.exists_rational_basis_projection line 66
  8. theorem OAI.Erdos3.exists_bounded_normalized_rational_image_basis line 89
  9. theorem OAI.Erdos3.exists_bounded_rational_projection_lift line 121
  10. def OAI.Erdos3.submoduleBasisMatrix line 204
  11. theorem OAI.Erdos3.realSubmoduleBasis_matrix_coordinates line 207
  12. theorem OAI.Erdos3.realSubmoduleBasis_matrix_span line 214
  13. def OAI.Erdos3.rationalCoordinateRealBasis line 241
  14. theorem OAI.Erdos3.rationalCoordinateRealBasis_apply line 244
  15. theorem OAI.Erdos3.realRationalCoordinateSpan_basis line 249
  16. theorem OAI.Erdos3.euclideanDerivative_bounded_horizontal_basis line 267
  17. theorem OAI.Erdos3.euclideanDerivative_rational_lift_matrix_data line 350
  18. def OAI.Erdos3.VectorPolynomial.rationalTagChartMatrix line 423
  19. theorem OAI.Erdos3.VectorPolynomial.rationalTagChartMatrix_same line 430
  20. theorem OAI.Erdos3.VectorPolynomial.rationalTagChartMatrix_of_ne line 436
  21. theorem OAI.Erdos3.VectorPolynomial.rationalTagChartMatrix_height line 442
  22. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.exists_bounded_chart_tag_basis line 455
  23. theorem OAI.Erdos3.VectorPolynomial.retained_tag_polynomial_coefficients_mem line 508