OAI/NumberTheory/PiExponent/Polynomials/WeightedPolynomialPole.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponent.WeightedPolynomialPole.coordinateOrderline 12 - def
OAI.PiExponent.WeightedPolynomialPole.coordinatePoleline 16 - theorem
OAI.PiExponent.WeightedPolynomialPole.realValuation_of_ne_zeroline 19 - theorem
OAI.PiExponent.WeightedPolynomialPole.coordinate_order_lowerline 27 - theorem
OAI.PiExponent.WeightedPolynomialPole.framePolynomial_order_lowerline 42