OAI/Combinatorics/Progressions/Geometry/FullTaggedChartCoefficientRange.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialTagLinearEmbedding line 15
  2. theorem OAI.Erdos3.polynomialTagLinearEmbedding_inl line 20
  3. theorem OAI.Erdos3.polynomialTagLinearEmbedding_inr line 23
  4. theorem OAI.Erdos3.polynomialTagLinearEmbedding_rename line 27
  5. theorem OAI.Erdos3.normalizedRealPolynomialChart_linear_restriction_coordinate line 34
  6. theorem OAI.Erdos3.normalizedRealPolynomialChart_linear_restriction line 53
  7. theorem OAI.Erdos3.polynomialTagLinearEmbedding_eval line 70
  8. theorem OAI.Erdos3.normalizedChart_decomposition_linear_restriction line 82
  9. theorem OAI.Erdos3.normalizedChart_coefficients_mem line 111
  10. def OAI.Erdos3.normalizedChartSubspaceCoordinates line 120
  11. theorem OAI.Erdos3.normalizedChartSubspaceCoordinates_coeff line 126
  12. theorem OAI.Erdos3.normalizedChartSubspaceCoordinates_reconstruct line 141
  13. theorem OAI.Erdos3.normalizedChartSubspaceCoordinates_eval_mem line 152
  14. theorem OAI.Erdos3.exists_normalizedChartSubspaceCoordinates line 168
  15. def OAI.Erdos3.polynomialSubspaceRestriction line 188
  16. theorem OAI.Erdos3.polynomialSubspaceRestriction_eval line 193
  17. theorem OAI.Erdos3.polynomialSubspaceRestriction_eq_of_eval line 200
  18. theorem OAI.Erdos3.polynomialSubspaceRestriction_eval_basis line 221
  19. theorem OAI.Erdos3.polynomialSubspaceRestriction_eval_eq line 234
  20. theorem OAI.Erdos3.normalizedChartSubspaceCoordinates_reconstruct_C line 242
  21. theorem OAI.Erdos3.polynomialSubspaceRestriction_normalizedChart line 250
  22. theorem OAI.Erdos3.polynomialSubspaceRestriction_normalizedChart_eval_eq line 263
  23. theorem OAI.Erdos3.normalizedChart_subspace_decomposition line 276
  24. def OAI.Erdos3.VectorPolynomial.fullTaggedMajorTopCoordinates line 313
  25. theorem OAI.Erdos3.VectorPolynomial.majorTranslationTopCoordinates_lowTagged_eq line 319
  26. theorem OAI.Erdos3.VectorPolynomial.lowTaggedMajorChart_rename line 335
  27. theorem OAI.Erdos3.VectorPolynomial.fullTaggedMajorChart_homogeneous line 355
  28. theorem OAI.Erdos3.VectorPolynomial.lowTaggedVectorExtend_majorChart line 371
  29. theorem OAI.Erdos3.VectorPolynomial.fullTaggedMajorTopCoordinates_coefficients_mem_of_all line 405
  30. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.exists_actual_normalized_chart_coordinates line 417
  31. theorem OAI.Erdos3.VectorPolynomial.fullTaggedMajorTopCoordinates_coefficients_mem_tag line 461
  32. theorem OAI.Erdos3.VectorPolynomial.fullTaggedMajorTopCoordinates_coefficients_mem line 488