IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.CoordinateUniqueness

declarations in this module (18)

• theorem natPrime_toNat_of_primeOrbit L31
• theorem primeOrbit_of_natPrime_toNat L53
• theorem primeOrbit_iff_natPrime_toNat L59
• def coordinateFactorization L71
• theorem coordinateFactorization_nil L75
• theorem coordinateFactorization_cons L79
• theorem primeCoordinateProduct_toNat_ne_zero L86
• theorem coordinateFactorization_eq_factorization_product L101
• theorem coordinateFactorization_eq_factorization_of_data L127
• theorem primeCoordinateData_factorization_unique L135
• theorem mem_coordinate_divides_product L144
• theorem coordinate_base_is_prime_divisor L162
• theorem mem_support_coordinateFactorization L176
• theorem prime_divisor_is_coordinate_base L200
• theorem primeOrbit_divides_iff_mem_coordinate_bases L223
• theorem classicalTransport_readout_is_canonical L240
• structure CoordinateUniquenessCertificate L248
• theorem coordinate_uniqueness_certificate L269