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
QRes(m,a)Exact expansion
exists qr_x_defined_qres. exists qr_u_defined_qres qr_v_defined_qres. qr_x_defined_qres * qr_x_defined_qres + m * qr_u_defined_qres = a + m * qr_v_defined_qresThis 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
PA005R quadratic_residue_bounded_equiv PA005S quadratic_residue_decidable_nonzero PA0087 quadratic_residue_mod_equiv PA008M quadratic_residue_half_power_mod_one PA009G scaled_inverse_no_fixed_of_not_qres PA009H scaled_inverse_prefix_no_fixed_of_not_qres PA009I scaled_inverse_prefix_choose_omitted_orbit PA009O scaled_inverse_pair_order_choose_append PA009T scaled_inverse_pair_order_paired_state_step PA009V scaled_inverse_pair_order_paired_iteration PA009W scaled_inverse_pair_order_terminal_package PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor PA00BM quadratic_nonresidue_half_power_mod_predecessor PA00BN bounded_euler_criterion_dichotomy 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 PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FM qres_same_status_from_even_count_sum 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 PA00FS qres_opposite_status_from_odd_count_sum 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