Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1QuotientTerm1

Recurrence 1 certificate: QuotientTerm1 #

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

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

Internal datum.

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

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm1_eq :
      recurrence1QuotientConstant * recurrence1Remainder21 = recurrence1QuotientTerm1