Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B1Square

Recurrence 6 certificate: B1Square #

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

source
noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence6B1SquareRows :
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.recurrence6B1SquareBands :
    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.remainder7Coefficient1Square_eq :
      remainder7Coefficient1Normalized * remainder7Coefficient1Normalized = remainder7Coefficient1Square