OAI/NumberTheory/PiExponent/Polynomials/PolynomialNormalNonzero.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.totalDegree_pderiv_lt_of_ne_zero line 10
2. theorem OAI.PiExponent.eq_constant_of_pderiv_eq_zero line 38
3. theorem OAI.PiExponent.ideal_eq_bot_of_pderiv_stable line 63
4. theorem OAI.PiExponent.polynomialPrimeNormal_mkQ_ne_zero line 91