OAI/Combinatorics/Progressions/Polynomial/PreparedFiniteNestedDegreeSourceProfileScalars.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.preparedFiniteNestedDegreeSourceProfile line 54
2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.preparedFiniteNestedDegreeSourceProfile_of_exponent line 233
3. theorem OAI.Erdos3.VectorPolynomial.nestedSourceFullScalar_and_rec line 257
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_preparedFiniteNestedDegreeSourceProfile_fullScalars line 304
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_preparedFiniteNestedDegreeSourceProfile_of_exponent_fullScalars line 392
6. theorem OAI.Erdos3.VectorPolynomial.nestedSourceScalar_and_rec line 480
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_preparedFiniteNestedDegreeSourceProfile_scalars line 527
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_preparedFiniteNestedDegreeSourceProfile_of_exponent_scalars line 612