NYLL
Module

Pic0_addOrderOf_mk_dvd_of_isPrincipal.lean

Nyll.JacobianVarieties.Pic0.Pic0_addOrderOf_mk_dvd_of_isPrincipal
1 declaration indexed from sourceView source ↗

Module documentation

The order of a degree-zero divisor class divides a principal multiple.

Imports2
Imported by1

Declarations

theorem

addOrderOf_mk_dvd_of_isPrincipal

L26 ↗
AlgebraicCurve.Pic0.addOrderOf_mk_dvd_of_isPrincipal
Source context 3 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_addOrderOf_mk_dvd_of_isPrincipal
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.addOrderOf_mk_dvd_of_isPrincipal {K F : Type*} [Field K]
    [Field F] [Algebra K F] (D : Divisor.degZero (K := K) (F := F)) (m : ℕ)
    (hD : Divisor.IsPrincipal (m • (D : Divisor K F))) : addOrderOf (Pic0.mk D) ∣ m

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