Documentation
MazurTorsion
.
Kubert
.
OrderSevenBacktrackingSelectionCertificateEval1
.
At6
Search
return to top
source
Imports
Init
Mathlib.Tactic.Ring
Mathlib.Tactic.SuppressCompilation
MazurTorsion.Kubert.OrderSevenBacktrackingSelectionCertificateEval0
Imported by
MazurTorsion
.
Kubert
.
OrderSevenBacktrackingCertificate
.
Internal
.
selectionEvalAt6
Selection-factor evaluation at 6
#
This shard verifies one independent rational abscissa.
source
theorem
MazurTorsion
.
Kubert
.
OrderSevenBacktrackingCertificate
.
Internal
.
selectionEvalAt6
(
d
:
ℚ
)
:
SelectionEvalCertificate
d
6