OAI/Combinatorics/Progressions/Estimates/PreparedCanonicalInitializedRelativeSource.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceLiteralRequired line 10
2. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceLiteralRequired_eq line 73
3. def OAI.Erdos3.VectorPolynomial.preparedCanonicalInitializedRelativeSourceDataConclusion line 95
4. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelative_initializerInputs line 374
5. def OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeLiteralRequired line 406
6. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeLiteralRequired_eq line 422
7. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeLiteralRequired_floors line 432
8. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalInitializedRelativeSourceCore line 460
9. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalInitializedRelativeSourceDataProof line 625
10. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCanonicalInitializedRelativeSource_of_data line 761
11. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCanonicalInitializedRelativeSource line 886