OAI/Combinatorics/Progressions/Lattices/IntegerHomogeneousSymbolPullbackGrid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.coordinate_realChartSubstitute_for_grid line 16
2. theorem OAI.Erdos3.VectorPolynomial.coefficientGrid_iff_coordinate line 27
3. theorem OAI.Erdos3.VectorPolynomial.CoefficientGrid.realChartSubstitute_integral line 45
4. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_homogeneousPullback_of_coefficientGrid line 66
5. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_homogeneousPullback_integral line 85
6. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_integerTopPullback line 97
7. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_integerTopPullback_of_coefficientGrid line 109