Module

Divisor_degree_nonneg_of_nonneg.lean

Nyll.AlgebraicCurves.Divisors.Divisor_degree_nonneg_of_nonneg

8 declarations indexed from sourceView source ↗

Module documentation

Divisor degree nonneg of nonneg

Imports4

Imported by2

theorem

ord_nonneg_of_mem

L31 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L47 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord
  f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg

L56 ↗

AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg.AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

degree_eq_sum_support

L69 ↗

AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg.AlgebraicCurve.Divisor.degree_eq_sum_support

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_eq_sum_support (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)

theorem

degree_nonneg_of_nonneg_port

L75 ↗

AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg_port

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_nonneg_of_nonneg_port [IsCurveOver K F]
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D

theorem

lSpace_eq_bot_of_degree_neg

L79 ↗

AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg.AlgebraicCurve.lSpace_eq_bot_of_degree_neg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem lSpace_eq_bot_of_degree_neg [IsCurveOver K F]
    (hD : Divisor.degree D < 0) : LSpace D = ⊥

theorem

ell_eq_zero_of_degree_neg

L95 ↗

AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg.AlgebraicCurve.ell_eq_zero_of_degree_neg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem ell_eq_zero_of_degree_neg [IsCurveOver K F] (hD : Divisor.degree D < 0) :
    ell D = 0

theorem

degree_nonneg_of_nonneg

L102 ↗

AlgebraicCurve.Divisor.degree_nonneg_of_nonneg

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Divisors.Proofs.DivisorDegreeNonnegNonneg.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg {K F : Type*} [Field K] [Field F]
  [Algebra K F] [IsCurveOver K F]
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D

Module documentation

Divisor degree nonneg of nonneg

Declarations