Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1QuotientTerm0

Recurrence 1 certificate: QuotientTerm0 #

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.recurrence1QuotientTerm0Rows :
Coefficient

Internal datum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0Bands :
    Coefficient

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1QuotientTerm0_eq :
      recurrence1QuotientConstant * recurrence1Remainder20 = recurrence1QuotientTerm0