Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6A2Square.Bands30To32

Recurrence 6 A2Square bands 30–32 #

This file checks bands 30 through 32 of an independent arithmetic product for recurrence 6.

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6A2SquareBand30_eq :
    recurrence6A2SquareBand30 = remainder6Coefficient2SquareBlock30
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6A2SquareBand31 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6A2SquareBand31_eq :
      recurrence6A2SquareBand31 = remainder6Coefficient2SquareBlock31
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6A2SquareBand32 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6A2SquareBand32_eq :
        recurrence6A2SquareBand32 = remainder6Coefficient2SquareBlock32