Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B0A2.Bands18To23

Recurrence 6 B0A2 bands 18–23 #

This file checks bands 18 through 23 of an independent arithmetic product for recurrence 6.

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band18_eq :
    recurrence6B0A2Band18 = remainder7Coefficient0TimesRemainder6Coefficient2Block18
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band19 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band19_eq :
      recurrence6B0A2Band19 = remainder7Coefficient0TimesRemainder6Coefficient2Block19
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band20 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band20_eq :
        recurrence6B0A2Band20 = remainder7Coefficient0TimesRemainder6Coefficient2Block20
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band21 :
        Coefficient

        Internal datum.

        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band21_eq :
          recurrence6B0A2Band21 = remainder7Coefficient0TimesRemainder6Coefficient2Block21
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band22 :
          Coefficient

          Internal datum.

          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band22_eq :
            recurrence6B0A2Band22 = remainder7Coefficient0TimesRemainder6Coefficient2Block22
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band23 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band23_eq :
              recurrence6B0A2Band23 = remainder7Coefficient0TimesRemainder6Coefficient2Block23