OAI/Combinatorics/Progressions/Geometry/CoordinateConstantDecomposition.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coordinateSiteValue line 12
  2. theorem OAI.Erdos3.VectorPolynomial.coordinateSiteValue_continuous line 18
  3. theorem OAI.Erdos3.VectorPolynomial.coordinateSiteValue_add line 28
  4. theorem OAI.Erdos3.VectorPolynomial.coordinateSiteValue_coefficientCoordinates line 43
  5. abbrev OAI.Erdos3.VectorPolynomial.ConstantCoefficientSlot line 89
  6. abbrev OAI.Erdos3.VectorPolynomial.NonconstantCoefficientSlot line 92
  7. instance OAI.Erdos3.VectorPolynomial.constantCoefficientSlotFintype line 95
  8. instance OAI.Erdos3.VectorPolynomial.nonconstantCoefficientSlotFintype line 98
  9. def OAI.Erdos3.VectorPolynomial.constantCoefficientSlotEquiv line 101
  10. abbrev OAI.Erdos3.VectorPolynomial.NonconstantCoordinateTori line 110
  11. def OAI.Erdos3.VectorPolynomial.coefficientConstantCoordinates line 114
  12. def OAI.Erdos3.VectorPolynomial.coefficientCoordinateSplit line 118
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientCoordinateSplit_measurePreserving line 123
  14. def OAI.Erdos3.VectorPolynomial.constantCoordinateExtension line 153
  15. def OAI.Erdos3.VectorPolynomial.nonconstantCoordinateExtension line 157
  16. theorem OAI.Erdos3.VectorPolynomial.nonconstantCoordinateExtension_continuous line 161
  17. theorem OAI.Erdos3.VectorPolynomial.coordinate_constant_decomposition line 171
  18. theorem OAI.Erdos3.VectorPolynomial.coordinateSiteValue_constant line 184
  19. theorem OAI.Erdos3.VectorPolynomial.coordinateSiteValue_split line 198