Module

RationalFunctionField_eq_placeInfty_of_ord_X_neg.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_eq_placeInfty_of_ord_X_neg

2 declarations indexed from sourceView source ↗

Module documentation

Rational Function Field eq place Infty of ord X neg

Imports4

Imported by2

theorem

eq_placeInfty_of_ord_X_neg

L38 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_eq_placeInfty_of_ord_X_neg.S09CD.eq_placeInfty_of_ord_X_neg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_eq_placeInfty_of_ord_X_neg
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
open AlgebraicCurve
namespace S09CD

Lean source · statement

theorem eq_placeInfty_of_ord_X_neg {K : Type*} [Field K] [DecidableEq (RatFunc K)] (v : Place K
  (RatFunc K))
    (hv : v.ord (RatFunc.X : RatFunc K) < 0) : v = RationalFunctionField.placeInfty K

theorem

eq_placeInfty_of_ord_X_neg

L51 ↗

AlgebraicCurve.RationalFunctionField.eq_placeInfty_of_ord_X_neg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_eq_placeInfty_of_ord_X_neg
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
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.eq_placeInfty_of_ord_X_neg {K : Type*} [Field
  K] [DecidableEq (RatFunc K)] (v : Place K (RatFunc K)) (hv : v.ord (RatFunc.X : RatFunc K) < 0) :
  v = RationalFunctionField.placeInfty K

Module documentation

Rational Function Field eq place Infty of ord X neg

Declarations

eq_placeInfty_of_ord_X_neg

eq_placeInfty_of_ord_X_neg