OAI/Combinatorics/Progressions/Lattices/AllocatedCommonPrimitiveAffine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedAffineGenuineKernelData line 37
2. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineGenuineKernelData_of_mixture line 176
3. def OAI.Erdos3.VectorPolynomial.AllocatedAccurateAffineData line 248
4. theorem OAI.Erdos3.VectorPolynomial.allocatedAccurateAffineData_of_mixture line 392
5. def OAI.Erdos3.VectorPolynomial.AllocatedNormalizedAffineData line 471
6. theorem OAI.Erdos3.VectorPolynomial.allocatedAccurateAffineData_normalized line 615
7. def OAI.Erdos3.VectorPolynomial.AllocatedPrimitiveAffineData line 725
8. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedAffineData_primitive line 866
9. def OAI.Erdos3.VectorPolynomial.AllocatedCommonAccurateAffineAt line 941
10. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonGenuineKernelAt_accurate_affine line 989
11. def OAI.Erdos3.VectorPolynomial.AllocatedCommonNormalizedAffineAt line 1038
12. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonAccurateAffineAt_normalized line 1086
13. def OAI.Erdos3.VectorPolynomial.AllocatedCommonPrimitiveAffineAt line 1170
14. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonNormalizedAffineAt_primitive line 1218