AlgebraicCurve.RationalFunctionField.ord_placeInfty_algebraMap
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ord_placeInfty_algebraMap
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionFieldLean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.ord_placeInfty_algebraMap {K : Type*} [Field K]
[DecidableEq (RatFunc K)] {q : Polynomial K} (hq : q ≠ 0) : (placeInfty K).ord (algebraMap
(Polynomial K) (RatFunc K) q) = -(q.natDegree : ℤ)