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 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
none
Used by conservative definitions
none
All transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
FS003Q four_square_parity_square_mod_two_self FS003R four_square_parity_pair_mod_two_sum FS003S four_square_parity_triple_mod_two_sum FS003T four_square_parity_norm_mod_two_sum FS0048 four_square_ordered_square_congruence_factors FS0049 four_square_ordered_half_square_injective FS004A four_square_prime_half_square_residues_injective FS004D four_square_equal_square_remainders_are_congruent FS004E four_square_half_square_residue_prefix_injective FS004N four_square_signed_conjugate_negative_blocks FS004O four_square_signed_natural_positive_first_blocks FS004P four_square_signed_cases_norm_quotient_zero_congruence FS004Q four_square_signed_orientation_mask_00 FS004R four_square_signed_orientation_mask_01 FS004S four_square_signed_orientation_mask_02 FS004T four_square_signed_orientation_mask_03 FS004U four_square_signed_orientation_mask_04 FS004V four_square_signed_orientation_mask_05 FS004W four_square_signed_orientation_mask_06 FS004X four_square_signed_orientation_mask_07 FS004Y four_square_signed_orientation_mask_08 FS004Z four_square_signed_orientation_mask_09 FS0050 four_square_signed_orientation_mask_10 FS0051 four_square_signed_orientation_mask_11 FS0052 four_square_signed_orientation_mask_12 FS0053 four_square_signed_orientation_mask_13 FS0054 four_square_signed_orientation_mask_14 FS0055 four_square_signed_orientation_mask_15 FS0057 four_square_signed_absolute_block_representation FS0058 four_square_signed_centered_representation FS0059 four_square_signed_lower_remainder_congruent FS005A four_square_signed_opposite_remainder_square_congruent FS005B four_square_signed_centered_square_congruent FS005C four_square_signed_centered_norm_congruent FS005D four_square_signed_centered_norm_quotient_exists FS005E four_square_signed_absolute_congruence_divisible FS005J four_square_signed_centered_orientation FS005K four_square_signed_negative_scale_zero FS005L four_square_signed_common_zero_cancel FS005M four_square_signed_cross_positive FS005N four_square_signed_cross_negative FS005O four_square_signed_cross_mixed_zero FS005P four_square_signed_mod_zero_add FS005Q four_square_signed_mod_zero_equivalent FS005R four_square_signed_mod_zero_swap FS005S four_square_signed_zero_cancel_right FS005T four_square_signed_cross_mixed_zero_reversed FS005U four_square_signed_dot_positive FS005V four_square_signed_dot_negative_zero FS005W four_square_signed_mod_zero_plus_congruent FS005X four_square_signed_partition_balance FS005Y four_square_signed_conjugate_positive_blocks FS005Z four_square_signed_conjugate_mixed_blocks FS0060 four_square_signed_natural_negative_first_blocksGrand-campaign planning vocabulary
Locate ModEq in the global campaign vocabulary →
Reviewed ModEq corresponds to blueprint ModEq with checked argument positions [0, 1, 2].
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.