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 conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
BT002W coprime_symm BT002X coprime_one_right BT002Y coprime_one_left BT0031 is_gcd_one_to_coprime BT0038 coprime_balanced_bezout BT0039 gauss_coprime_cancel BT003N euclid_prime_dvd_product BT004F binary_crt BT004I beta_modulus_coprime_base BT004K beta_moduli_coprime_of_gap_dvd BT004O beta_moduli_coprime_of_lt_bounded_common_multiple BT004P beta_moduli_pairwise_coprime_bounded BT004R coprime_mul_left BT004S coprime_mul_right BT004U binary_crt_fold_step BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT005B beta_exclusive_recode_invariant_step BT005C bounded_beta_exclusive_recode_invariant BT005D beta_prefix_extend BT008Q prime_coprime_or_divides BT008R prime_not_divides_coprime BT008S distinct_primes_coprime BT00BG coprime_product_is_lcm BT00DH beta_product_pointwise_coprime BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00VE primorial_interval_pairwise_coprime BT00VF primorial_interval_divides_choose_between BT00YU coprime_power_right BT00YV coprime_powers BT00YW prime_contribution_prefix_pairwise_coprime BT00YY prime_contribution_product_divides