Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B1Square.Bands10To18

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.recurrence6B1SquareBand10 :
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.recurrence6B1SquareBand10_eq :
    recurrence6B1SquareBand10 = remainder7Coefficient1SquareBlock10
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand11 :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand11_eq :
      recurrence6B1SquareBand11 = remainder7Coefficient1SquareBlock11
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand12 :
      Coefficient

      Internal datum.

      Instances For
        source
        theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand12_eq :
        recurrence6B1SquareBand12 = remainder7Coefficient1SquareBlock12
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand13 :
        Coefficient

        Internal datum.

        Instances For
          source
          theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand13_eq :
          recurrence6B1SquareBand13 = remainder7Coefficient1SquareBlock13
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand14 :
          Coefficient

          Internal datum.

          Instances For
            source
            theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand14_eq :
            recurrence6B1SquareBand14 = remainder7Coefficient1SquareBlock14
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand15 :
            Coefficient

            Internal datum.

            Instances For
              source
              theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand15_eq :
              recurrence6B1SquareBand15 = remainder7Coefficient1SquareBlock15
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand16 :
              Coefficient

              Internal datum.

              Instances For
                source
                theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand16_eq :
                recurrence6B1SquareBand16 = remainder7Coefficient1SquareBlock16
                source
                noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand17 :
                Coefficient

                Internal datum.

                Instances For
                  source
                  theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand17_eq :
                  recurrence6B1SquareBand17 = remainder7Coefficient1SquareBlock17
                  source
                  noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand18 :
                  Coefficient

                  Internal datum.

                  Instances For
                    source
                    theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareBand18_eq :
                    recurrence6B1SquareBand18 = remainder7Coefficient1SquareBlock18