AlgebraicCurve.residueTheorem_of_isAlgClosed
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheorem_of_isAlgClosed
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.residueTheorem_of_isAlgClosed
{K F : Type*} [Field K] [IsAlgClosed K]
[Field F] [Algebra K F]
[AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
[∀ w : AlgebraicCurve.Place K F, w.DCoordGenerates]
[Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
[Algebra.IsIntegral (RatFunc K) F] [Module.Finite (RatFunc K) F]
[AlgebraicCurve.HasLocalResidue K F]
[∀ w : AlgebraicCurve.Place K F, w.FiniteResidue]
[Nontrivial Ω[F⁄K]]
(hcurve : AlgebraicCurve.IsCurveOver K F)
[AlgebraicCurve.IsCurveOver K (RatFunc K)]
[∀ u : AlgebraicCurve.Place K (RatFunc K), u.FiniteResidue]
[AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
[Algebra.IsSeparable (RatFunc K) F]
[Nontrivial Ω[(RatFunc K)⁄K]] [∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates] :
∀ [AlgebraicCurve.HasPrincipalDivisors K F], AlgebraicCurve.ResidueTheorem K F