Module

HasCanonicalLocalResidueK.lean

Nyll.AlgebraicCurves.Differentials.Residues.HasCanonicalLocalResidueK

1 declaration indexed from sourceView source ↗

Module documentation

Has Canonical Local Residue K

Imports2

Imported by4

theorem

hasCanonicalLocalResidueK

AlgebraicCurve.hasCanonicalLocalResidueK

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.HasCanonicalLocalResidueK
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.hasCanonicalLocalResidueK
    (K F : Type*) [Field K] [Field F] [Algebra K F] :
    AlgebraicCurve.HasCanonicalLocalResidueK K F