Documentation
MazurTorsion
.
Kubert
.
OrderSevenIsogenyDoublingCertificateEval2
Search
return to top
source
Imports
Init
Mathlib.Tactic.FinCases
Mathlib.Tactic.NormNum
Mathlib.Tactic.Ring
MazurTorsion.Kubert.OrderSevenIsogenyDoublingCertificateEval1
Imported by
MazurTorsion
.
Kubert
.
OrderSevenDoublingCertificate
.
Internal
.
evalBlock2
source
theorem
MazurTorsion
.
Kubert
.
OrderSevenDoublingCertificate
.
Internal
.
evalBlock2
(
d
:
ℚ
)
(
i
:
Fin
4
)
:
EvalCertificate
d
(
↑
↑
i
+
8
)