OAI/Combinatorics/Progressions/Polynomial/PolynomialPatchNoPivotGlobalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialPatch.ofTranslatedShearOrbit line 12
2. theorem OAI.Erdos3.PolynomialPatch.ofTranslatedShearOrbit_weight line 19
3. theorem OAI.Erdos3.PolynomialPatch.ofTranslatedShearOrbit_kernel line 24
4. theorem OAI.Erdos3.PolynomialPatch.ofTranslatedShearOrbit_value_integer line 29
5. theorem OAI.Erdos3.PolynomialPatch.exists_patch_of_kernelProjection_scores line 59
6. theorem OAI.Erdos3.PolynomialPatch.exists_noPivot_ambient_patch line 127