NYLL
Module

Divisor_degree_eq_sum.lean

Nyll.AlgebraicCurves.Divisors.Divisor_degree_eq_sum
1 declaration indexed from sourceView source ↗

Module documentation

Compute the degree of a divisor as a sum of weighted coefficients.

Imports1
Imported by3

Declarations

theorem

degree_eq_sum

L30 ↗
AlgebraicCurve.Divisor.degree_eq_sum
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_degree_eq_sum
open IsDedekindDomain WithZero IsLocalRing
open AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.degree_eq_sum {K F : Type*} [Field K] [Field F] [Algebra K
    F] (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)

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