OAI/Combinatorics/Progressions/Lattices/AffineLiftInsertion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.affineLiftSubstitution line 13
2. theorem OAI.Erdos3.affineLiftSubstitution_degree line 18
3. theorem OAI.Erdos3.affineLiftSubstitution_eval line 37
4. def OAI.Erdos3.PolynomialPatch.insertAffineLifts line 45
5. theorem OAI.Erdos3.PolynomialPatch.insertAffineLifts_lip line 51
6. theorem OAI.Erdos3.PolynomialPatch.insertAffineLifts_value_at_lift line 57
7. theorem OAI.Erdos3.PolynomialPatch.exists_affine_lift_insertion line 70