Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B0A2.Bands24To25

Recurrence 6 B0A2 bands 24–25 #

This file checks bands 24 through 25 of an independent arithmetic product for recurrence 6.

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band24_eq :
    recurrence6B0A2Band24 = remainder7Coefficient0TimesRemainder6Coefficient2Block24
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band25 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band25_eq :
      recurrence6B0A2Band25 = remainder7Coefficient0TimesRemainder6Coefficient2Block25