Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantCertificateData6

Step 6 data for the order-seven branch-zero resultant PRS #

This serial data shard records one normalized primitive remainder and exceptional content factor. Its linear pseudo-division quotient is derived from leading coefficients and checked by the Lean recurrence.

source
noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder8Coefficient0Chunk0 :
Coefficient
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder8Coefficient0Block0 :
    Coefficient
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder8Coefficient0 :
      Coefficient
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder8 :
        Bivariate
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.quotient6 :
          Bivariate
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptionalUnit6 :
            Coefficient
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptional6 :
              Coefficient
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6 :
                Prop
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For