Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence1Bridge

Recurrence 1 certificate: Bridge #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient0_eq_normalized :
divisionCofactor0Coefficient0 = recurrence1Source0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient1_eq_normalized :
divisionCofactor0Coefficient1 = recurrence1Source1
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient2_eq_normalized :
divisionCofactor0Coefficient2 = recurrence1Source2
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient3_eq_normalized :
divisionCofactor0Coefficient3 = recurrence1Source3
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient4_eq_normalized :
divisionCofactor0Coefficient4 = recurrence1Source4
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient5_eq_normalized :
divisionCofactor0Coefficient5 = recurrence1Source5
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient6_eq_normalized :
divisionCofactor0Coefficient6 = recurrence1Source6
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.divisionCofactor0Coefficient7_eq_normalized :
divisionCofactor0Coefficient7 = recurrence1Source7
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient0_eq_normalized :
remainder2Coefficient0 = recurrence1Remainder20
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient1_eq_normalized :
remainder2Coefficient1 = recurrence1Remainder21
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient2_eq_normalized :
remainder2Coefficient2 = recurrence1Remainder22
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient3_eq_normalized :
remainder2Coefficient3 = recurrence1Remainder23
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient4_eq_normalized :
remainder2Coefficient4 = recurrence1Remainder24
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient5_eq_normalized :
remainder2Coefficient5 = recurrence1Remainder25
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder2Coefficient6_eq_normalized :
remainder2Coefficient6 = recurrence1Remainder26
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder3Coefficient0_eq_normalized :
remainder3Coefficient0 = recurrence1Remainder30
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder3Coefficient1_eq_normalized :
remainder3Coefficient1 = recurrence1Remainder31
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder3Coefficient2_eq_normalized :
remainder3Coefficient2 = recurrence1Remainder32
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder3Coefficient3_eq_normalized :
remainder3Coefficient3 = recurrence1Remainder33
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder3Coefficient4_eq_normalized :
remainder3Coefficient4 = recurrence1Remainder34
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder3Coefficient5_eq_normalized :
remainder3Coefficient5 = recurrence1Remainder35
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptional1_eq_normalized :
exceptional1 = recurrence1Exceptional