Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B0A2.Bands6To11

Recurrence 6 B0A2 bands 6–11 #

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

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

Internal datum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band6_eq :
    recurrence6B0A2Band6 = remainder7Coefficient0TimesRemainder6Coefficient2Block6
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band7 :
    Coefficient

    Internal datum.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band7_eq :
      recurrence6B0A2Band7 = remainder7Coefficient0TimesRemainder6Coefficient2Block7
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band8 :
      Coefficient

      Internal datum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band8_eq :
        recurrence6B0A2Band8 = remainder7Coefficient0TimesRemainder6Coefficient2Block8
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band9 :
        Coefficient

        Internal datum.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band9_eq :
          recurrence6B0A2Band9 = remainder7Coefficient0TimesRemainder6Coefficient2Block9
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band10 :
          Coefficient

          Internal datum.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band10_eq :
            recurrence6B0A2Band10 = remainder7Coefficient0TimesRemainder6Coefficient2Block10
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band11 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B0A2Band11_eq :
              recurrence6B0A2Band11 = remainder7Coefficient0TimesRemainder6Coefficient2Block11