Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6Term1.Rows15To17

Recurrence 6 Term1 rows 15–17 #

This file checks an independent group of row identities for Term1 of the sixth pseudo-division recurrence.

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

Internal datum.

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

    Internal datum.

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

      Internal datum.

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

        Internal datum.

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

          Internal datum.

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

            Internal datum.

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

              Internal datum.

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

                Internal datum.

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

                  Internal datum.

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

                    Internal datum.

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

                      Internal datum.

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

                        Internal datum.

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

                          Internal datum.

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

                            Internal datum.

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

                              Internal datum.

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

                                Internal datum.

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

                                  Internal datum.

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

                                    Internal datum.

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

                                      Internal datum.

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

                                        Internal datum.

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

                                          Internal datum.

                                          Instances For
                                            source
                                            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Row15_eq :
                                            remainder6Coefficient0NormalizedBlock15 * remainder7Coefficient1Square = recurrence6Term1Row15
                                            source
                                            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Row16Band16 :
                                            Coefficient

                                            Internal datum.

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

                                              Internal datum.

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

                                                Internal datum.

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

                                                  Internal datum.

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

                                                    Internal datum.

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

                                                      Internal datum.

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

                                                        Internal datum.

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

                                                          Internal datum.

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

                                                            Internal datum.

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

                                                              Internal datum.

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

                                                                Internal datum.

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

                                                                  Internal datum.

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

                                                                    Internal datum.

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

                                                                      Internal datum.

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

                                                                        Internal datum.

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

                                                                          Internal datum.

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

                                                                            Internal datum.

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

                                                                              Internal datum.

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

                                                                                Internal datum.

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

                                                                                  Internal datum.

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

                                                                                    Internal datum.

                                                                                    Instances For
                                                                                      source
                                                                                      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Row16_eq :
                                                                                      remainder6Coefficient0NormalizedBlock16 * remainder7Coefficient1Square = recurrence6Term1Row16
                                                                                      source
                                                                                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Row17Band17 :
                                                                                      Coefficient

                                                                                      Internal datum.

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

                                                                                        Internal datum.

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

                                                                                          Internal datum.

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

                                                                                            Internal datum.

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

                                                                                              Internal datum.

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

                                                                                                Internal datum.

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

                                                                                                  Internal datum.

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

                                                                                                    Internal datum.

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

                                                                                                      Internal datum.

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

                                                                                                        Internal datum.

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

                                                                                                          Internal datum.

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

                                                                                                            Internal datum.

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

                                                                                                              Internal datum.

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

                                                                                                                Internal datum.

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

                                                                                                                  Internal datum.

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

                                                                                                                    Internal datum.

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

                                                                                                                      Internal datum.

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

                                                                                                                        Internal datum.

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

                                                                                                                          Internal datum.

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

                                                                                                                            Internal datum.

                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Row17_eq :
                                                                                                                              remainder6Coefficient0NormalizedBlock17 * remainder7Coefficient1Square = recurrence6Term1Row17