IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility

declarations in this module (31)

• def one L27
• theorem one_toNat L30
• theorem one_ne_zero L34
• theorem mul_one_eq L39
• theorem one_mul_eq L44
• theorem mul_assoc L48
• def divides L56
• def unit L61
• def nontrivialFactorization L65
• def primeOrbit L71
• theorem divides_refl L74
• theorem divides_zero L78
• theorem one_divides L82
• theorem divides_trans L86
• theorem divides_mul_right L94
• theorem divides_mul_left L98
• theorem zero_divides_iff_eq_zero L103
• theorem divides_iff_toNat_dvd L115
• theorem unit_iff_toNat_eq_one L131
• theorem divides_one_iff_unit L142
• theorem unit_of_divides_unit L147
• theorem divides_antisymm L155
• theorem ofNat_ne_zero_of_ne_zero L163
• theorem not_unit_ofNat_of_ne_one L170
• theorem nontrivialFactorization_iff_toNat L179
• theorem primeOrbit_iff_toNat_no_nontrivial_factor L220
• theorem unit_or_unit_of_mul_eq_prime L243
• theorem primeOrbit_of_unit_or_unit L266
• theorem unit_or_eq_of_divides_prime L279
• structure OrbitDivisibilityCertificate L291
• theorem orbit_divisibility_certificate L332