Module

RationalFunctionField_degree_eq_zero_of_forall_eq_ord.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_degree_eq_zero_of_forall_eq_ord

1 declaration indexed from sourceView source ↗

Module documentation

RationalFunctionField degree eq zero of forall eq ord

The orders of a nonzero rational function form a divisor of degree zero.

Imports4

Imported by14

theorem

degree_eq_zero_of_forall_eq_ord

L41 ↗

AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_forall_eq_ord

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_forall_eq_ord {K : Type*}
  [Field K] {f : RatFunc K} (D : Divisor K (RatFunc K)) (hD : ∀ v : Place K (RatFunc K), D v =
  v.ord f) : Divisor.degree D = 0

Module documentation

RationalFunctionField degree eq zero of forall eq ord

Declarations

degree_eq_zero_of_forall_eq_ord