Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1ShiftTerm1

Recurrence 1 certificate: ShiftTerm1 #

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

Internal datum.

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

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1ShiftTerm1_eq :
      recurrence1Remainder26 * recurrence1Remainder20 = recurrence1ShiftTerm1