OAI/Combinatorics/Progressions/Polynomial/PolynomialPatchResidualCell.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.PolynomialSlots.takePrefixline 13 - theorem
OAI.Erdos3.PolynomialSlots.takePrefix_slotsline 18 - theorem
OAI.Erdos3.PolynomialPatch.exists_freeze_of_residual_cellline 47 - theorem
OAI.Erdos3.TriangularSlots.takePrefix_zeroline 74 - theorem
OAI.Erdos3.PolynomialPatch.exists_constant_of_residual_cellline 89