Module

Pic0_nsmul_mk_eq_zero_of_isPrincipal.lean

Nyll.JacobianVarieties.Pic0.Pic0_nsmul_mk_eq_zero_of_isPrincipal

1 declaration indexed from sourceView source ↗

Module documentation

A principal natural multiple of a divisor annihilates its degree-zero Picard class.

Imports2

Nyll.AlgebraicCurves.Divisors.ClassGroup
Nyll.JacobianVarieties.Pic0.Pic0_zsmul_mk_eq_zero_of_isPrincipal

Imported by2

Nyll.JacobianVarieties.Pic0.All
Nyll.JacobianVarieties.Pic0.Pic0_addOrderOf_mk_dvd_of_isPrincipal

theorem

nsmul_mk_eq_zero_of_isPrincipal

L26 ↗

AlgebraicCurve.Pic0.nsmul_mk_eq_zero_of_isPrincipal

Source context 3 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_nsmul_mk_eq_zero_of_isPrincipal
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Pic0.nsmul_mk_eq_zero_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))) : m • Pic0.mk D = 0

Module documentation

Declarations

nsmul_mk_eq_zero_of_isPrincipal