Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1ShiftTerm1.Rows3To5

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.recurrence1ShiftTerm1Row3Band3 :
Coefficient

Internal datum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band4 :
    Coefficient

    Internal datum.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band5 :
      Coefficient

      Internal datum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band6 :
        Coefficient

        Internal datum.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band7 :
          Coefficient

          Internal datum.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band8 :
            Coefficient

            Internal datum.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band9 :
              Coefficient

              Internal datum.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band10 :
                Coefficient

                Internal datum.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band11 :
                  Coefficient

                  Internal datum.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band12 :
                    Coefficient

                    Internal datum.

                    Instances For
                      source
                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band13 :
                      Coefficient

                      Internal datum.

                      Instances For
                        source
                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band14 :
                        Coefficient

                        Internal datum.

                        Instances For
                          source
                          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band15 :
                          Coefficient

                          Internal datum.

                          Instances For
                            source
                            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band16 :
                            Coefficient

                            Internal datum.

                            Instances For
                              source
                              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3Band17 :
                              Coefficient

                              Internal datum.

                              Instances For
                                source
                                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row3 :
                                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.recurrence1ShiftTerm1Row3_eq :
                                  recurrence1Remainder26Block3 * recurrence1Remainder20 = recurrence1ShiftTerm1Row3
                                  source
                                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band4 :
                                  Coefficient

                                  Internal datum.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band5 :
                                    Coefficient

                                    Internal datum.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band6 :
                                      Coefficient

                                      Internal datum.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band7 :
                                        Coefficient

                                        Internal datum.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band8 :
                                          Coefficient

                                          Internal datum.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band9 :
                                            Coefficient

                                            Internal datum.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band10 :
                                              Coefficient

                                              Internal datum.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band11 :
                                                Coefficient

                                                Internal datum.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band12 :
                                                  Coefficient

                                                  Internal datum.

                                                  Instances For
                                                    source
                                                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band13 :
                                                    Coefficient

                                                    Internal datum.

                                                    Instances For
                                                      source
                                                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band14 :
                                                      Coefficient

                                                      Internal datum.

                                                      Instances For
                                                        source
                                                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band15 :
                                                        Coefficient

                                                        Internal datum.

                                                        Instances For
                                                          source
                                                          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band16 :
                                                          Coefficient

                                                          Internal datum.

                                                          Instances For
                                                            source
                                                            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band17 :
                                                            Coefficient

                                                            Internal datum.

                                                            Instances For
                                                              source
                                                              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4Band18 :
                                                              Coefficient

                                                              Internal datum.

                                                              Instances For
                                                                source
                                                                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row4 :
                                                                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.recurrence1ShiftTerm1Row4_eq :
                                                                  recurrence1Remainder26Block4 * recurrence1Remainder20 = recurrence1ShiftTerm1Row4
                                                                  source
                                                                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band5 :
                                                                  Coefficient

                                                                  Internal datum.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    source
                                                                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band6 :
                                                                    Coefficient

                                                                    Internal datum.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      source
                                                                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band7 :
                                                                      Coefficient

                                                                      Internal datum.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        source
                                                                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band8 :
                                                                        Coefficient

                                                                        Internal datum.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          source
                                                                          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band9 :
                                                                          Coefficient

                                                                          Internal datum.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            source
                                                                            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band10 :
                                                                            Coefficient

                                                                            Internal datum.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              source
                                                                              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band11 :
                                                                              Coefficient

                                                                              Internal datum.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                source
                                                                                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band12 :
                                                                                Coefficient

                                                                                Internal datum.

                                                                                Instances For
                                                                                  source
                                                                                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band13 :
                                                                                  Coefficient

                                                                                  Internal datum.

                                                                                  Instances For
                                                                                    source
                                                                                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band14 :
                                                                                    Coefficient

                                                                                    Internal datum.

                                                                                    Instances For
                                                                                      source
                                                                                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band15 :
                                                                                      Coefficient

                                                                                      Internal datum.

                                                                                      Instances For
                                                                                        source
                                                                                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band16 :
                                                                                        Coefficient

                                                                                        Internal datum.

                                                                                        Instances For
                                                                                          source
                                                                                          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band17 :
                                                                                          Coefficient

                                                                                          Internal datum.

                                                                                          Instances For
                                                                                            source
                                                                                            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band18 :
                                                                                            Coefficient

                                                                                            Internal datum.

                                                                                            Instances For
                                                                                              source
                                                                                              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5Band19 :
                                                                                              Coefficient

                                                                                              Internal datum.

                                                                                              Instances For
                                                                                                source
                                                                                                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1Row5 :
                                                                                                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.recurrence1ShiftTerm1Row5_eq :
                                                                                                  recurrence1Remainder26Block5 * recurrence1Remainder20 = recurrence1ShiftTerm1Row5