OAI/Combinatorics/Progressions/Polynomial/WeightedPolynomialEndomorphisms.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.weightedPolynomialEndDropline 13 - theorem
OAI.Erdos3.weightedPolynomialEndDrop_antitoneline 24 - theorem
OAI.Erdos3.weightedPolynomialEndDrop_mulline 29 - theorem
OAI.Erdos3.weightedPolynomialEndDrop_oneline 38 - theorem
OAI.Erdos3.weightedPolynomialEndDrop_terminalline 44 - def
OAI.Erdos3.weightedPolynomialEndAlgebraline 53 - instance
OAI.Erdos3.weightedPolynomialEndAlgebraRingline 58 - theorem
OAI.Erdos3.polynomialShearEnd_mem_dropline 63 - def
OAI.Erdos3.weightedPolynomialEndLayerline 69 - def
OAI.Erdos3.weightedPolynomialEndFiltrationline 73