AlgebraicCurve.residueTheorem_of_residueTheoremK
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheorem_of_residueTheoremK
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.residueTheorem_of_residueTheoremK
{K F : Type*} [Field K] [Field F] [Algebra K F]
[AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
[AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
[∀ v : AlgebraicCurve.Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
(h : AlgebraicCurve.ResidueTheoremK K F) :
∀ [AlgebraicCurve.HasPrincipalDivisors K F], AlgebraicCurve.ResidueTheorem K F