Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B1Square.Bands0To9

Recurrence 6 certificate: B1Square #

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

source
noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand0 :
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.recurrence6B1SquareBand0_eq :
    recurrence6B1SquareBand0 = remainder7Coefficient1SquareBlock0
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand1 :
    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.recurrence6B1SquareBand1_eq :
      recurrence6B1SquareBand1 = remainder7Coefficient1SquareBlock1
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand2 :
      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.recurrence6B1SquareBand2_eq :
        recurrence6B1SquareBand2 = remainder7Coefficient1SquareBlock2
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand3 :
        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.recurrence6B1SquareBand3_eq :
          recurrence6B1SquareBand3 = remainder7Coefficient1SquareBlock3
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand4 :
          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.recurrence6B1SquareBand4_eq :
            recurrence6B1SquareBand4 = remainder7Coefficient1SquareBlock4
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand5 :
            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.recurrence6B1SquareBand5_eq :
              recurrence6B1SquareBand5 = remainder7Coefficient1SquareBlock5
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand6 :
              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.recurrence6B1SquareBand6_eq :
                recurrence6B1SquareBand6 = remainder7Coefficient1SquareBlock6
                source
                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand7 :
                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.recurrence6B1SquareBand7_eq :
                  recurrence6B1SquareBand7 = remainder7Coefficient1SquareBlock7
                  source
                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand8 :
                  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.recurrence6B1SquareBand8_eq :
                    recurrence6B1SquareBand8 = remainder7Coefficient1SquareBlock8
                    source
                    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand9 :
                    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.recurrence6B1SquareBand9_eq :
                      recurrence6B1SquareBand9 = remainder7Coefficient1SquareBlock9