NYLL
Module

RationalFunctionField_ord_placeInfty.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeInfty
1 declaration indexed from sourceView source ↗

Module documentation

RationalFunctionField ord placeInfty

The order of a nonzero rational function at infinity is the negative of its integer degree.

Imports7
Imported by22

Declarations

theorem

ord_placeInfty

L38 ↗
AlgebraicCurve.RationalFunctionField.ord_placeInfty
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ord_placeInfty
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 IsDedekindDomain AlgebraicCurve AlgebraicCurve.RationalFunctionField
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.ord_placeInfty {K : Type*} [Field K]
  [DecidableEq (RatFunc K)] {f : RatFunc K} (hf : f ≠ 0) : (placeInfty K).ord f = -f.intDegree

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.