NYLL
Module

TateAgreement_v2.lean

Nyll.AlgebraicCurves.Differentials.Residues.TateAgreement_v2
1 declaration indexed from sourceView source ↗

Module documentation

Compare the second Tate residue constructions.

Imports15
Imported by2

Declarations

theorem

tateAgreement_v2

L38 ↗
AlgebraicCurve.tateAgreement_v2
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateAgreement_v2
Lean source · statement
theorem _root_.AlgebraicCurve.tateAgreement_v2
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [AlgebraicCurve.IsCurveOver K L] [PerfectField K]
    [∀ u : AlgebraicCurve.Place K L, u.FiniteResidue]
    (hfin : ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite K L) :
    ModularCurve.KwF4gRRTate.KwF4gRRTateAgreement K L hfin

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.