Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
¬a = 0 ∧ FpMul(p,a,b,1)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~(((a)) = 0)) /\ ((((exists pfa_gap_bottomlayermultiplicationleft. pfa_gap_bottomlayermultiplicationleft + S ((a)) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplicationright. pfa_gap_bottomlayermultiplicationright + S ((b)) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplicationresultbound. pfa_gap_bottomlayermultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplicationresultcongruence pfa_offset_right_bottomlayermultiplicationresultcongruence. (((a)) * ((b))) + ((p)) * pfa_offset_left_bottomlayermultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayermultiplicationresultcongruence)))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
PX0026 · prime_field_polynomial_inverse_scalePX0027 · prime_field_polynomial_quotient_scalar_cancellationPX002F · prime_field_polynomial_quotient_prefix_convolution_entryPX0030 · prime_field_polynomial_quotient_prefix_product_matchesPX0031 · prime_field_polynomial_quotient_prefix_remainder_zeroPX0037 · prime_field_polynomial_division_quotient_data_existsPX0039 · prime_field_polynomial_division_execution_existsPX0057 · prime_field_polynomial_division_quotient_data_functional