Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B1A1.Bands12To17

Recurrence 6 B1A1 bands 12–17 #

This file checks bands 12 through 17 of an independent arithmetic product for recurrence 6.

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band12_eq :
    recurrence6B1A1Band12 = remainder7Coefficient1TimesRemainder6Coefficient1Block12
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band13 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band13_eq :
      recurrence6B1A1Band13 = remainder7Coefficient1TimesRemainder6Coefficient1Block13
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band14 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band14_eq :
        recurrence6B1A1Band14 = remainder7Coefficient1TimesRemainder6Coefficient1Block14
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band15 :
        Coefficient

        Internal datum.

        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band15_eq :
          recurrence6B1A1Band15 = remainder7Coefficient1TimesRemainder6Coefficient1Block15
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band16 :
          Coefficient

          Internal datum.

          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band16_eq :
            recurrence6B1A1Band16 = remainder7Coefficient1TimesRemainder6Coefficient1Block16
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band17 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1A1Band17_eq :
              recurrence6B1A1Band17 = remainder7Coefficient1TimesRemainder6Coefficient1Block17