Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1QuotientTerm0.Bands13To24

Recurrence 1 certificate: QuotientTerm0 #

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

Internal datum.

Instances For
    source
    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band13_eq :
    recurrence1QuotientTerm0Band13 = recurrence1QuotientTerm0Block13
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band14 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band14_eq :
      recurrence1QuotientTerm0Band14 = recurrence1QuotientTerm0Block14
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band15 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band15_eq :
        recurrence1QuotientTerm0Band15 = recurrence1QuotientTerm0Block15
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band16 :
        Coefficient

        Internal datum.

        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band16_eq :
          recurrence1QuotientTerm0Band16 = recurrence1QuotientTerm0Block16
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band17 :
          Coefficient

          Internal datum.

          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band17_eq :
            recurrence1QuotientTerm0Band17 = recurrence1QuotientTerm0Block17
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band18 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band18_eq :
              recurrence1QuotientTerm0Band18 = recurrence1QuotientTerm0Block18
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band19 :
              Coefficient

              Internal datum.

              Instances For
                source
                theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band19_eq :
                recurrence1QuotientTerm0Band19 = recurrence1QuotientTerm0Block19
                source
                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band20 :
                Coefficient

                Internal datum.

                Instances For
                  source
                  theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band20_eq :
                  recurrence1QuotientTerm0Band20 = recurrence1QuotientTerm0Block20
                  source
                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band21 :
                  Coefficient

                  Internal datum.

                  Instances For
                    source
                    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band21_eq :
                    recurrence1QuotientTerm0Band21 = recurrence1QuotientTerm0Block21
                    source
                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band22 :
                    Coefficient

                    Internal datum.

                    Instances For
                      source
                      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band22_eq :
                      recurrence1QuotientTerm0Band22 = recurrence1QuotientTerm0Block22
                      source
                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band23 :
                      Coefficient

                      Internal datum.

                      Instances For
                        source
                        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band23_eq :
                        recurrence1QuotientTerm0Band23 = recurrence1QuotientTerm0Block23
                        source
                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band24 :
                        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.recurrence1QuotientTerm0Band24_eq :
                          recurrence1QuotientTerm0Band24 = recurrence1QuotientTerm0Block24