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 ≤ bOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists h. h + a = bThe unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Checked theorems using this definition
PX0001 · polynomial_diagonal_left_prefix_transportPX0002 · polynomial_diagonal_prefix_left_transportPX0003 · prime_field_convolution_coefficient_prefix_transportPX000A · prime_field_polynomial_left_pad_index_casesPX000B · prime_field_polynomial_power_index_before_paddingPX000C · prime_field_polynomial_power_coefficient_existsPX001A · prime_field_polynomial_left_pad_power_coefficientPX002A · prime_field_polynomial_quotient_prefix_restrictPX0030 · prime_field_polynomial_quotient_prefix_product_matchesPX0031 · prime_field_polynomial_quotient_prefix_remainder_zeroPX0032 · polynomial_quotient_length_existsPX0033 · polynomial_quotient_length_boundsPX0034 · prime_field_polynomial_trim_zero_prefix_cut_boundPX0035 · prime_field_polynomial_trim_zero_prefix_remainder_boundPX0036 · prime_field_polynomial_trim_bounded_degreePX0037 · prime_field_polynomial_division_quotient_data_existsPX003A · prime_field_polynomial_division_remainder_degreePX0056 · prime_field_polynomial_trim_input_transportPX0075 · prime_field_polynomial_add_equivalent_congruentPX0076 · prime_field_polynomial_subtract_equivalent_congruentPX0077 · prime_field_polynomial_convolution_equivalent_congruent_leftPX0078 · prime_field_polynomial_convolution_equivalent_congruent_right