Module

WeilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists.lean

Nyll.AlgebraicCurves.Cohomology.WeilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists

1 declaration indexed from sourceView source ↗

Module documentation

Weil Duality Adelic of function Field Riemann Roch of stichtenoth Genus Exists

Imports4

Imported by13

theorem

weilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists

L29 ↗

AlgebraicCurve.weilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.WeilDualityAdelicFunctionField
open AlgebraicCurve

Lean source · statement

theorem
  _root_.AlgebraicCurve.weilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (hRR : AlgebraicCurve.FunctionFieldRiemannRoch K F)
    (hSG : AlgebraicCurve.StichtenothGenusExists K F) :
    AlgebraicCurve.WeilDualityAdelic K F

Module documentation

Weil Duality Adelic of function Field Riemann Roch of stichtenoth Genus Exists

Declarations

weilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists