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, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.
Definition neighborhood
Depends on conservative definitions
Used by conservative definitions
CF0013 PrimitivePythagorean ND0070 EuclidParameters ND0074 EuclidParametrization ND0071 PrimitiveFermatFourCounterexampleAll transitive conservative prerequisites
Used by theorem statements or local proof propositions
PF000B pythagorean_coprime_swap PF000N pythagorean_odd_coordinate_coprime_two PF000P pythagorean_square_gap_coprime_first_parameter PF000Q pythagorean_square_gap_coprime_second_parameter PF000R pythagorean_square_gap_coprime_parameter_product PF000S pythagorean_primitive_euclidean_legs PF000T pythagorean_primitive_euclidean_constructor PF000U pythagorean_primitive_euclidean_from_order PF000V pythagorean_primitive_euclidean_swapped_constructor PF000W pythagorean_primitive_hypotenuse_coprime_first_leg PF000X pythagorean_primitive_hypotenuse_coprime_second_leg PF000Y pythagorean_primitive_pairwise_coprime PF0017 pythagorean_primitive_normal_form PF001D coprime_square_reduced_factors PF001E coprime_square_product_factors PF001F square_divides_square_reduced_root PF001G square_divides_square_root PF001N pythagorean_half_factors_coprime PF001O pythagorean_coprime_square_roots PF001V pythagorean_odd_even_half_factors PF001W pythagorean_half_factors_extract_parameters PF001X pythagorean_primitive_odd_even_inverse PF0022 pythagorean_positive_primitive_from_parameters PF0026 fermat_four_coprime_squares PF002E fermat_four_odd_double_square_factors PF002F fermat_four_primitive_normalization PF002G fermat_four_nested_primitive_triangle PF002H fermat_four_second_parameter_descentGrand-campaign planning vocabulary
Locate Coprime in the global campaign vocabulary →
Reviewed Coprime corresponds to blueprint Coprime with checked argument positions [0, 1].
The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.