OAI/Combinatorics/Progressions/Polynomial/StrongRefiltrationRealPolynomialLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_unique_quotient_fiber_polynomial_lift line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_unique_adapted_quotient_fiber_polynomial_lift line 70
3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_unique_quotient_fiber_polynomialOrbit_lift line 96
4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_unique_real_quotient_fiber_polynomialOrbit_lift line 139
5. theorem OAI.Erdos3.NilpotentLieFiltration.real_polynomialOrbit_formal_map_eval line 226
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_unique_refiltered_quotient_polynomialOrbit_lift line 268
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_unique_real_refiltered_quotient_polynomialOrbit_lift line 320