Module

ExistsUnique_hasSimpleResidue_of_hasSimplePoleAt.lean

Nyll.AlgebraicCurves.Differentials.Residues.ExistsUnique_hasSimpleResidue_of_hasSimplePoleAt

2 declarations indexed from sourceView source ↗

Module documentation

Exists Unique has Simple Residue of has Simple Pole At

Imports4

Imported by3

theorem

main

L33 ↗

AlgebraicCurves.Differentials.Residues.Proofs.ExistsUnique_hasSimpleResidue_of_hasSimplePoleAt.ResEx.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace ExistsUnique_hasSimpleResidue_of_hasSimplePoleAt
open AlgebraicCurve
namespace ResEx
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem main [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    (v : Place K F) (ω : Ω[F⁄K]) (hω : v.HasSimplePoleAt ω) :
    ∃! a : K, v.HasSimpleResidue ω a

theorem

existsUnique_hasSimpleResidue_of_hasSimplePoleAt

L54 ↗

AlgebraicCurve.existsUnique_hasSimpleResidue_of_hasSimplePoleAt

Source context 4 commands