Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6Term1.Bands0To5

Recurrence 6 Term1 bands 0–5 #

This file checks an independent group of band identities for Term1 of the sixth pseudo-division recurrence.

source
noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band0 :
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.recurrence6Term1Band0_eq :
    recurrence6Term1Band0 = normalizedResidual6Term1Block0
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band1 :
    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.recurrence6Term1Band1_eq :
      recurrence6Term1Band1 = normalizedResidual6Term1Block1
      source
      noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band2 :
      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.recurrence6Term1Band2_eq :
        recurrence6Term1Band2 = normalizedResidual6Term1Block2
        source
        noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band3 :
        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.recurrence6Term1Band3_eq :
          recurrence6Term1Band3 = normalizedResidual6Term1Block3
          source
          noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band4 :
          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.recurrence6Term1Band4_eq :
            recurrence6Term1Band4 = normalizedResidual6Term1Block4
            source
            noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Band5 :
            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.recurrence6Term1Band5_eq :
              recurrence6Term1Band5 = normalizedResidual6Term1Block5