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
BalancedInverse(m,a,b)Exact expansion
exists dp_u dp_v. (a) * (b) + m * dp_u = 1 + m * dp_vThis 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
Used by theorem statements or local proof propositions
PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA005D predecessor_square_mod_one PA005E pow_predecessor_parity_mod PA0062 prime_mod_inverse PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA008N scaled_inverse_from_unit_inverse PA00AG prime_bounded_square_one_cases PA00AP inverse_prefix_last_fixed PA00B7 paired_successor_lift_adjacent_units PA00B8 paired_pair_order_factor_code_exists PA00B9 beta_adjacent_unit_pairs_product_one PA00BA paired_pair_order_product_one_exists PA00BE prime_wilson_terminal_product_package_exists PA00BF prime_terminal_range_two_product_mod_one_exists