OAI/Combinatorics/Progressions/Estimates/AllocatedActualNormalizedTupleComparison.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedActualScalarTupleStatement line 14
2. def OAI.Erdos3.VectorPolynomial.allocatedConstructedTupleTail line 194
3. def OAI.Erdos3.VectorPolynomial.allocatedConstructedScalarTupleTail line 285
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_scalar_tuple_comparison line 403
5. def OAI.Erdos3.VectorPolynomial.allocatedPrimitiveScalarStatement line 519
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_primitive_scalar_tuple_comparison line 608
7. theorem OAI.Erdos3.VectorPolynomial.allocatedConstructedScalarTail_of_original line 660
8. theorem OAI.Erdos3.VectorPolynomial.allocatedActualScalarTupleComparison line 748
9. theorem OAI.Erdos3.VectorPolynomial.allocatedActualScalarTupleComparison_withProjection line 778
10. theorem OAI.Erdos3.VectorPolynomial.allocatedActualNormalizedTupleComparison line 808