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
∃ u. ∃ v. a + m · u = b + m · vOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists u v. a + m * u = b + m * vThe 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
PX0040 · beta_sum_pointwise_mod_addPX0041 · polynomial_zero_extended_add_congruentPX0042 · polynomial_diagonal_term_left_add_congruentPX0043 · polynomial_diagonal_term_right_add_congruentPX0044 · polynomial_diagonal_sum_left_add_congruentPX0045 · polynomial_diagonal_sum_right_add_congruentPX0046 · prime_field_convolution_coefficient_left_addPX0047 · prime_field_convolution_coefficient_right_add