Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Readable signature
Coprime(a,b)Exact expansion
forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
PA000P coprime_one_left PA0015 beta_modulus_coprime_base PA001M coprime_balanced_bezout PA001P gauss_coprime_cancel PA001Q beta_moduli_coprime_of_gap_dvd PA001R beta_moduli_coprime_of_lt_bounded_common_multiple PA001S beta_moduli_pairwise_coprime_bounded PA001T coprime_mul_left PA001U beta_exclusive_accumulated_product_step PA0026 binary_crt PA0028 binary_crt_fold_step PA002G beta_exclusive_recode_congruence_step PA002H beta_exclusive_recode_invariant_step PA002I bounded_beta_exclusive_recode_invariant PA002X beta_prefix_extend PA0037 is_gcd_one_to_coprime PA0038 euclid_prime_dvd_product PA003M prime_coprime_or_divides PA003N prime_not_divides_coprime PA003O coprime_symm PA003P coprime_balanced_mod_inverse PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA003S prime_mod_cancel PA0062 prime_mod_inverse PA0081 beta_product_pointwise_coprime PA0082 prime_positive_bounded_product_coprime PA0083 prime_half_range_product_coprime PA0084 gauss_signed_products_cancel_mod PA008K prime_range_product_coprime PA008L fermat_predecessor_exponent_mod_one