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
ModEq(m,a,b)Exact expansion
exists u v. a + m * u = b + m * 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
none
Used by definitions
PD0021 QRes PD0022 BoundedQRes PD0031 BalancedInverse PD0033 ScaledInverse PD0034 ScaledFixedPoint PD0035 SuccessorInverseUsed by theorem statements or local proof propositions
PA001W bezout_mod_left PA001X bezout_mod_right PA001Y mod_eq_mul_right PA0020 mod_eq_mul_left PA0021 dvd_to_mod_zero PA0022 mod_eq_add PA0023 mod_eq_refl PA0024 mod_eq_trans PA0025 mod_eq_predecessor_cancel PA0026 binary_crt PA0027 mod_eq_of_mod_eq_multiple PA0028 binary_crt_fold_step PA002G beta_exclusive_recode_congruence_step PA002H beta_exclusive_recode_invariant_step PA002I bounded_beta_exclusive_recode_invariant PA002U mod_eq_bounded_unique PA002V mod_eq_to_remainder_decomposition PA002W beta_at_of_mod_eq_bound PA002X beta_prefix_extend PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA003P coprime_balanced_mod_inverse PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA003S prime_mod_cancel PA004E mod_eq_mul PA005E pow_predecessor_parity_mod PA005I pow_mod_congruent PA005J mod_eq_decidable_from_remainders PA005K mod_eq_decidable_nonzero PA005L quadratic_residue_search_up_to PA005M quadratic_residue_bounded_decidable_nonzero PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0070 gauss_pointwise_signed_half_representative PA0071 gauss_pointwise_signed_half_choice PA0072 gauss_half_range_signed_choices PA0073 gauss_signed_half_prefix_extend PA0074 gauss_signed_half_prefix_exists PA0075 gauss_half_range_signed_prefix_exists PA0076 gauss_signed_half_prefix_all_bits PA0077 gauss_signed_half_bit_count_exists PA0078 gauss_signed_half_magnitude_range PA0079 prime_scaled_same_target_unique PA007A gauss_same_sign_scaled_source_unique PA007B gauss_mixed_sign_scaled_source_impossible PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA007P gauss_signed_pointwise_mul_scale_mod PA007Q beta_product_pointwise_scale_mod PA007R gauss_signed_pointwise_mul_product_mod PA0080 gauss_signed_products_balance_mod PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA0086 nondivisor_canonical_remainder_exists PA0087 quadratic_residue_mod_equiv PA0088 pow_congruent_base_witness PA008A mod_eq_zero_to_dvd_nonzero PA008B prime_mul_index_map_exists_up_to PA008D fermat_index_map_bounded PA008E prime_mul_index_map_injective PA008H beta_successor_range_scale_mod PA008I prime_mul_residue_reindex_exists PA008J prime_mul_residue_product_balance PA008L fermat_predecessor_exponent_mod_one PA008M quadratic_residue_half_power_mod_one PA008N scaled_inverse_from_unit_inverse PA008O scaled_inverse_transport_right PA008P prime_scaled_inverse_target_nonzero PA008Q prime_scaled_inverse_exists PA009C prime_scaled_inverse_unique PA009X scaled_pair_order_successor_lift_adjacent_targets PA00A0 beta_adjacent_target_pairs_product_power PA00AO inverse_prefix_zero_fixed 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 PA00BI mod_one_product_restore_predecessor PA00BJ prime_factorial_wilson_congruence PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor PA00BM quadratic_nonresidue_half_power_mod_predecessor PA00BN bounded_euler_criterion_dichotomy PA00BP odd_prime_one_not_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BU arbitrary_euler_criterion_complete PA00BV arbitrary_gauss_lemma_complete PA00C4 predecessor_multiple_mod_complement PA00C5 canonical_remainder_from_mod PA00C6 odd_signed_division_branch_exact PA00CH even_to_mod_two_zero PA00CI odd_to_mod_two_one PA00CJ matching_parity_mod_two PA00CK odd_product_division_mod_two PA00CL odd_reflected_remainder_mod_two PA00CM signed_remainder_sum_mod_two PA00CN odd_scaled_division_signed_mod_two PA00CO odd_signed_division_congruence_mod_two PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00CR gauss_eisenstein_terminal_sums_mod_two PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum PA00D1 mod_eq_add_cancel_left PA00D2 mod_two_cancel_middle PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two PA00D4 mod_two_zero_to_even PA00D5 mod_two_zero_sum_to_congruent PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FH gauss_count_sum_mod_two_from_quotient_sums PA00FK mod_two_one_to_odd PA00FL mod_two_preserves_parity PA00FN qres_same_status_from_even_half_product_mod_two PA00FO qres_same_status_from_mod_four_one PA00FP conditional_qres_same_status_from_oriented_gauss_counts PA00FT qres_opposite_status_from_odd_half_product_mod_two PA00FU qres_opposite_status_from_mod_four_three PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts PA00FW quadratic_reciprocity_combined