OAI/Combinatorics/Progressions/Polynomial/PreparedPolynomialPullback.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.ofCoordinates_eq_sum_tmul line 14
2. theorem OAI.Erdos3.VectorPolynomial.substitute_ofCoordinates line 22
3. theorem OAI.Erdos3.VectorPolynomial.substitute_integerCoordinates line 29
4. def OAI.Erdos3.RankPreparationLayer.pullback line 44
5. theorem OAI.Erdos3.RankPreparationLayer.pullback_space line 57
6. theorem OAI.Erdos3.RankPreparationLayer.pullback_rank line 60
7. theorem OAI.Erdos3.RankPreparationLayer.Valid.pullback line 63
8. def OAI.Erdos3.RankPreparationFamily.pullback line 75
9. theorem OAI.Erdos3.RankPreparationFamily.pullback_polynomial line 78
10. theorem OAI.Erdos3.RankPreparationFamily.pullback_identity line 83