Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6Term1.Bands30To35

Recurrence 6 Term1 bands 30–35 #

This file checks an independent group of band identities for Term1 of the sixth pseudo-division recurrence.

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band30_eq :
    recurrence6Term1Band30 = normalizedResidual6Term1Block30
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band31 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band31_eq :
      recurrence6Term1Band31 = normalizedResidual6Term1Block31
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band32 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band32_eq :
        recurrence6Term1Band32 = normalizedResidual6Term1Block32
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band33 :
        Coefficient

        Internal datum.

        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band33_eq :
          recurrence6Term1Band33 = normalizedResidual6Term1Block33
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band34 :
          Coefficient

          Internal datum.

          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band34_eq :
            recurrence6Term1Band34 = normalizedResidual6Term1Block34
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band35 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band35_eq :
              recurrence6Term1Band35 = normalizedResidual6Term1Block35