Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence6B1A1

Recurrence 6 certificate: B1A1 #

This compatibility module combines independently checked row and band shards for the recurrence-6 B1A1 arithmetic product.

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

Internal datum.

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

    Internal datum.

    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1TimesRemainder6Coefficient1_eq :
      remainder7Coefficient1Normalized * remainder6Coefficient1Normalized = remainder7Coefficient1TimesRemainder6Coefficient1