Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1QuotientTerm0.Bands0To12

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.recurrence1QuotientTerm0Band0 :
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.recurrence1QuotientTerm0Band0_eq :
    recurrence1QuotientTerm0Band0 = recurrence1QuotientTerm0Block0
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band1 :
    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.recurrence1QuotientTerm0Band1_eq :
      recurrence1QuotientTerm0Band1 = recurrence1QuotientTerm0Block1
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band2 :
      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.recurrence1QuotientTerm0Band2_eq :
        recurrence1QuotientTerm0Band2 = recurrence1QuotientTerm0Block2
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band3 :
        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.recurrence1QuotientTerm0Band3_eq :
          recurrence1QuotientTerm0Band3 = recurrence1QuotientTerm0Block3
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band4 :
          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.recurrence1QuotientTerm0Band4_eq :
            recurrence1QuotientTerm0Band4 = recurrence1QuotientTerm0Block4
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band5 :
            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.recurrence1QuotientTerm0Band5_eq :
              recurrence1QuotientTerm0Band5 = recurrence1QuotientTerm0Block5
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band6 :
              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.recurrence1QuotientTerm0Band6_eq :
                recurrence1QuotientTerm0Band6 = recurrence1QuotientTerm0Block6
                source
                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band7 :
                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.recurrence1QuotientTerm0Band7_eq :
                  recurrence1QuotientTerm0Band7 = recurrence1QuotientTerm0Block7
                  source
                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band8 :
                  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.recurrence1QuotientTerm0Band8_eq :
                    recurrence1QuotientTerm0Band8 = recurrence1QuotientTerm0Block8
                    source
                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band9 :
                    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.recurrence1QuotientTerm0Band9_eq :
                      recurrence1QuotientTerm0Band9 = recurrence1QuotientTerm0Block9
                      source
                      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band10 :
                      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.recurrence1QuotientTerm0Band10_eq :
                        recurrence1QuotientTerm0Band10 = recurrence1QuotientTerm0Block10
                        source
                        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band11 :
                        Coefficient

                        Internal datum.

                        Instances For
                          source
                          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band11_eq :
                          recurrence1QuotientTerm0Band11 = recurrence1QuotientTerm0Block11
                          source
                          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band12 :
                          Coefficient

                          Internal datum.

                          Instances For
                            source
                            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Band12_eq :
                            recurrence1QuotientTerm0Band12 = recurrence1QuotientTerm0Block12