OAI/Combinatorics/Progressions/Estimates/CopiedLayerSpace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.copiedLayerSpace line 12
  2. def OAI.Erdos3.VectorPolynomial.copiedLayerSpaceEquiv line 19
  3. theorem OAI.Erdos3.VectorPolynomial.copiedLayerSpace_finrank line 29
  4. theorem OAI.Erdos3.VectorPolynomial.copiedLayerSpace_line_finrank line 34
  5. def OAI.Erdos3.VectorPolynomial.copiedLayerMatrix line 39
  6. def OAI.Erdos3.VectorPolynomial.copiedLayerRows line 46
  7. theorem OAI.Erdos3.VectorPolynomial.copiedLayerMatrix_height line 49
  8. theorem OAI.Erdos3.VectorPolynomial.copiedLayerRows_height line 60
  9. theorem OAI.Erdos3.VectorPolynomial.copiedLayerMatrix_real_mulVec line 68
  10. theorem OAI.Erdos3.VectorPolynomial.copiedLayerRows_real_mulVec line 77
  11. theorem OAI.Erdos3.VectorPolynomial.jointRationalSpace_copiedLayer line 85
  12. def OAI.Erdos3.VectorPolynomial.copyLeft line 117
  13. def OAI.Erdos3.VectorPolynomial.copyRight line 122
  14. def OAI.Erdos3.VectorPolynomial.copiedLayerPolynomial line 127
  15. theorem OAI.Erdos3.VectorPolynomial.coefficients_copiedLayerPolynomial line 131
  16. theorem OAI.Erdos3.VectorPolynomial.copiedLayerPolynomial_mem line 137
  17. theorem OAI.Erdos3.VectorPolynomial.copiedLayerPolynomial_degree line 146
  18. theorem OAI.Erdos3.VectorPolynomial.eval_copiedLayerPolynomial line 155