Documentation
Atlas
.
ArithmeticGeometry
.
code
.
BSDConjecture
Search
return to top
source
Imports
Init
Mathlib
Atlas.ArithmeticGeometry.code.TateShafarevich
Imported by
EllipticCurveOver
.
LFunction
EllipticCurveOver
.
mordellWeilRank
EllipticCurveOver
.
LFunction_analyticAt
birch_swinnerton_dyer_conjecture
source
noncomputable def
EllipticCurveOver
.
LFunction
(
E
:
EllipticCurveOver
ℚ
)
:
ℂ
→
ℂ
Instances For
source
noncomputable def
EllipticCurveOver
.
mordellWeilRank
(
E
:
EllipticCurveOver
ℚ
)
:
ℕ
Instances For
source
theorem
EllipticCurveOver
.
LFunction_analyticAt
(
E
:
EllipticCurveOver
ℚ
)
:
AnalyticAt
ℂ
E
.
LFunction
1
source
theorem
birch_swinnerton_dyer_conjecture
(
E
:
EllipticCurveOver
ℚ
)
:
analyticOrderAt
E
.
LFunction
1
=
↑
E
.
mordellWeilRank