OAI/NumberTheory/PiExponent/Polynomials/ColonHilbertPolynomial.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponentJets.W64.shiftHilbertPolynomialline 11 - theorem
OAI.PiExponentJets.W64.shiftHilbertPolynomial_evalline 14 - theorem
OAI.PiExponentJets.W64.shiftHilbertPolynomial_natDegreeline 19 - theorem
OAI.PiExponentJets.W64.shiftHilbertPolynomial_leadingCoeffline 24 - theorem
OAI.PiExponentJets.W64.shiftHilbertPolynomial_top_coeffline 31 - theorem
OAI.PiExponentJets.W64.hilbertMultiplicity_shiftline 48 - theorem
OAI.PiExponentJets.W64.hilbertMultiplicity_addline 54 - theorem
OAI.PiExponentJets.W64.colon_hilbert_polynomial_eventuallyline 58 - theorem
OAI.PiExponentJets.W64.colon_hilbert_polynomial_multiplicityline 83