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
IsGCD(g,a,b)Exact expansion
((exists x. a = g * x) /\ (exists y. b = g * y)) /\ forall d. (exists u. a = d * u) -> (exists v. b = d * v) -> exists w. g = d * wThis 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
PA001F is_gcd_zero_right PA001H is_gcd_euclid_forward PA001K gcd_balanced_bezout_exists_up_to PA001L gcd_balanced_bezout_exists PA001M coprime_balanced_bezout PA0035 gcd_exists_up_to PA0036 gcd_exists_relational PA0037 is_gcd_one_to_coprime PA0038 euclid_prime_dvd_product PA003M prime_coprime_or_divides