AlgebraicCurve.Pic0.subsingleton_of_forall_isPrincipal
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_subsingleton_of_forall_isPrincipal
open IsDedekindDomain WithZero IsLocalRing
open AlgebraicCurve inLean source · statement
theorem _root_.AlgebraicCurve.Pic0.subsingleton_of_forall_isPrincipal (K F : Type*) [Field K]
[Field F] [Algebra K F]
(h : ∀ D : Divisor K F, Divisor.degree D = 0 → D.IsPrincipal) :
Subsingleton (Pic0 K F)