Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1ShiftTerm1.Bands12To23

Recurrence 1 certificate: ShiftTerm1 #

This file is a checked bounded-band arithmetic shard for the first pseudo-division recurrence in the order-seven branch-zero resultant certificate.

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band12_eq :
    recurrence1ShiftTerm1Band12 = recurrence1ShiftTerm1Block12
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band13 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band13_eq :
      recurrence1ShiftTerm1Band13 = recurrence1ShiftTerm1Block13
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band14 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band14_eq :
        recurrence1ShiftTerm1Band14 = recurrence1ShiftTerm1Block14
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band15 :
        Coefficient

        Internal datum.

        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band15_eq :
          recurrence1ShiftTerm1Band15 = recurrence1ShiftTerm1Block15
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band16 :
          Coefficient

          Internal datum.

          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band16_eq :
            recurrence1ShiftTerm1Band16 = recurrence1ShiftTerm1Block16
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band17 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band17_eq :
              recurrence1ShiftTerm1Band17 = recurrence1ShiftTerm1Block17
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band18 :
              Coefficient

              Internal datum.

              Instances For
                source
                theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band18_eq :
                recurrence1ShiftTerm1Band18 = recurrence1ShiftTerm1Block18
                source
                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band19 :
                Coefficient

                Internal datum.

                Instances For
                  source
                  theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band19_eq :
                  recurrence1ShiftTerm1Band19 = recurrence1ShiftTerm1Block19
                  source
                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band20 :
                  Coefficient

                  Internal datum.

                  Instances For
                    source
                    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band20_eq :
                    recurrence1ShiftTerm1Band20 = recurrence1ShiftTerm1Block20
                    source
                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band21 :
                    Coefficient

                    Internal datum.

                    Instances For
                      source
                      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band21_eq :
                      recurrence1ShiftTerm1Band21 = recurrence1ShiftTerm1Block21
                      source
                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band22 :
                      Coefficient

                      Internal datum.

                      Instances For
                        source
                        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band22_eq :
                        recurrence1ShiftTerm1Band22 = recurrence1ShiftTerm1Block22
                        source
                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band23 :
                        Coefficient

                        Internal datum.

                        Instances For
                          source
                          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Band23_eq :
                          recurrence1ShiftTerm1Band23 = recurrence1ShiftTerm1Block23