OAI/NumberTheory/PiExponent/Polynomials/MixedSlopePolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial line 9
2. lemma OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial_eval line 12
3. lemma OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial_eval_zero line 18
4. theorem OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial_derivative line 23
5. lemma OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial_derivative_eval line 42
6. theorem OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial_eval_div line 48
7. lemma OAI.PiExponent.NumericalAmpleness.mixedSlopePolynomial_natDegree_le line 61