Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6Term1

Recurrence 6 certificate: Term1 #

This compatibility module combines the independently checked row and band shards for Term1 of the sixth pseudo-division recurrence.

source
noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Rows :
Coefficient

Internal datum.

Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6Term1Bands :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.normalizedResidual6Term1_eq :
      remainder6Coefficient0Normalized * remainder7Coefficient1Square = normalizedResidual6Term1