Polynomial data for the order-seven backtracking certificates #
This file stores the degree-33 selection cofactor and the three canonical
degree-seven quotient cofactors as nested polynomials in ℚ[D][X]. The
pointwise ℚ[X] factors are obtained only by specializing the inner parameter
variable, so the large coefficient tables have a single source of truth.
The quotient factors are ordered by constant-term D-valuation 3, 2, and
1; this is the canonical order used by the FLINT resultant computation.
Computational provenance #
The coefficient tables were generated with SymPy polynomial arithmetic over
ℚ[x,d]. The computation expanded the order-seven Tate and selection
formulas, formed the selection numerator and the quotient seventh division
polynomial, divided each exactly by the displayed dual-kernel cubic, factored
the quotient cofactor, and sorted its three factors by constant-term
d-valuation 3, 2, and 1. SymPy specialization at the integer
abscissas emitted the Horner expressions in the evaluation shards. The Lean
ring proofs in those shards and the interpolation argument in the final
certificate check the emitted data; they do not trust the generating script.
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk9 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0Chunk10 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk9 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1Chunk10 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2Chunk9 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3Chunk9 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk9 :
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4Chunk9 = 52968752573 + Polynomial.X * (878056515 + Polynomial.X * (3509609 + Polynomial.X * -3988))
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5Chunk9 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7Chunk8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8Chunk8 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient8 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient9 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10Chunk7 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient10 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk7 :
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11Chunk7 = 1011284737 + Polynomial.X * (2136058 + Polynomial.X * -685)
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient11 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient12 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13Chunk6 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient13 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk6 :
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14Chunk6 = 283877623812 + Polynomial.X * (186376308 + Polynomial.X * (-7146547 + Polynomial.X * 2064))
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient14 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15Chunk6 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient15 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient16 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17Chunk5 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient17 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18Chunk5 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient18 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient19Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient19Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient19Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient19Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient19Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient19 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient20Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient20Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient20Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient20Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient20Chunk4 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient20 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient21Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient21Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient21Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient21Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient21Chunk4 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient21 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient22Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient22Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient22Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient22Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient22 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient23Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient23Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient23Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient23Chunk3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient23 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient24Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient24Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient24Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient24Chunk3 :
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient24Chunk3 = -368513012 + Polynomial.X * (1678063 + Polynomial.X * -137)
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient24 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient25Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient25Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient25Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient25 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient26Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient26Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient26Chunk2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient26 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient27Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient27Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient27Chunk2 :
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient27Chunk2 = 128511613 + Polynomial.X * (21289862 + Polynomial.X * (-48415 + Polynomial.X * -1))
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient27 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient28Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient28Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient28 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient29Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient29Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient29 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient30Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient30Chunk1 :
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient30Chunk1 = 36490480 + Polynomial.X * (-3503950 + Polynomial.X * (-321873 + Polynomial.X * -174))
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient30 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient31Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient31 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient32Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient32 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient33Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionCofactorCoefficient33 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient0Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient0Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient0Chunk2 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient1Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient1Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient2Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient2Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient3Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient3Chunk1 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient4Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient4 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient5Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient5 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient6Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient6 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient7Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor0Coefficient7 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient0Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient0Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient0Chunk2 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient1Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient1Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient2Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient2Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient3Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient3Chunk1 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient4Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient4 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient5Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient5 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient6Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient6 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient7Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor1Coefficient7 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient0Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient0Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient0Chunk2 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient1Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient1Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient2Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient2Chunk1 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient2 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient3Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient3Chunk1 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient3 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient4Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient4 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient5Chunk0 :
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient5 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient6Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient6 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient7Chunk0 :
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.divisionCofactor2Coefficient7 :
Internal datum.
Equations
Instances For
The degree-33 selection cofactor, stored over the parameter ring ℚ[D].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first canonical degree-seven quotient cofactor (constant-term valuation 3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second canonical degree-seven quotient cofactor (constant-term valuation 2).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third canonical degree-seven quotient cofactor (constant-term valuation 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Specialization of the selection cofactor at the parameter d.
Equations
Instances For
Specialization of the first quotient cofactor at the parameter d.
Equations
Instances For
Specialization of the second quotient cofactor at the parameter d.
Equations
Instances For
Specialization of the third quotient cofactor at the parameter d.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.dualKernelPolynomial
(d : ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.completedCubicPolynomial
(W : WeierstrassCurve ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.completedTangentPolynomial
(W : WeierstrassCurve ℚ)
:
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.tateAlphaPolynomial
(W : WeierstrassCurve ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.tateGammaPolynomial
(W : WeierstrassCurve ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.tateParameterNumeratorPolynomial
(W : WeierstrassCurve ℚ)
:
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.tateParameterDenominatorPolynomial
(W : WeierstrassCurve ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.parameterCubicPolynomial
(A B : Polynomial ℚ)
:
Internal datum.
Equations
- MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.parameterCubicPolynomial A B = A ^ 3 - Polynomial.C 8 * A ^ 2 * B + Polynomial.C 5 * A * B ^ 2 + B ^ 3
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.parameterHauptmodulNumeratorPolynomial
(A B : Polynomial ℚ)
:
Internal datum.
Equations
Instances For
noncomputable def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.selectionPolynomialData
(d : ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.SelectionEvalCertificate
(d n : ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.quotient_prePsiSeven
(d : ℚ)
:
(orderSevenQuotient d).preΨ' 7 = ((orderSevenQuotient d).preΨ₄ * (orderSevenQuotient d).Ψ₂Sq ^ 2 - (orderSevenQuotient d).Ψ₃ ^ 3) * (orderSevenQuotient d).Ψ₃ ^ 3 - (orderSevenQuotient d).preΨ₄ ^ 3 * (orderSevenQuotient d).Ψ₂Sq ^ 2
def
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.DivisionEvalCertificate
(d n : ℚ)
:
Internal datum.
Equations
- One or more equations did not get rendered due to their size.