Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupExceptionalData

Recurrence 5 lookup certificate: exceptional polynomial data #

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

source
noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalizedBlock0 :
Coefficient

Internal datum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalizedBlock1 :
    Coefficient

    Internal datum.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalizedBlock2 :
      Coefficient

      Internal datum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalizedBlock3 :
        Coefficient

        Internal datum.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalizedBlock4 :
          Coefficient

          Internal datum.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalizedBlock5 :
            Coefficient

            Internal datum.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalNormalized :
              Coefficient

              Internal datum.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptional5_eq_recurrence5ExceptionalNormalized :
                exceptional5 = exceptionalUnit5 * recurrence5ExceptionalNormalized