IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean

declarations in this module (36)

• def divModFuel L28
• def divMod L39
• def quotient L43
• def remainder L47
• theorem divModFuel_toNat_aux L50
• theorem divMod_toNat L94
• theorem quotient_toNat L107
• theorem remainder_toNat L112
• theorem remainder_lt_divisor L117
• theorem quotient_mul_divisor_add_remainder_eq L129
• def gcdFuel L140
• def gcd L153
• def coprime L157
• theorem gcdFuel_toNat_aux L160
• theorem gcd_toNat L220
• theorem coprime_iff_nat_coprime L226
• theorem gcd_divides_left L231
• theorem gcd_divides_right L237
• theorem divides_gcd_of_divides_left_right L243
• theorem coprime_divides_of_divides_mul_left L255
• theorem gcd_ne_zero_of_right_ne_zero L264
• theorem quotient_mul_divisor_toNat_of_divides L275
• theorem quotient_ne_zero_of_divides L281
• def signedQuotient L297
• theorem signedQuotient_abs_toNat L305
• theorem signedQuotient_mul_divisor_toInt_of_divides L328
• def normalizeRatio L366
• theorem normalizeRatio_num_mul_gcd_toInt L379
• theorem normalizeRatio_den_mul_gcd_toNat L388
• theorem normalizeRatio_toRat L397
• theorem normalizeRatio_crossEq L429
• theorem normalizeRatio_coprime L434
• def RatioNormalizationTarget L457
• theorem ratio_normalization_target L463
• structure OrbitEuclideanCertificate L468
• theorem orbit_euclidean_certificate L499