NYLL
Module

Pic0_mk_eq_zero_iff.lean

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

Module documentation

Pic0 mk eq zero iff

Imports1
Imported by8

Declarations

theorem

mk_eq_zero_iff

L25 ↗
AlgebraicCurve.Pic0.mk_eq_zero_iff
Source context 3 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_mk_eq_zero_iff
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.mk_eq_zero_iff {K F : Type*} [Field K] [Field F] [Algebra K F]
  (D : Divisor.degZero (K := K) (F := F)) : Pic0.mk D = 0 ↔ Divisor.IsPrincipal (D : Divisor K F)

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