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.
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
DL0004 · matrix_recursive_prefix_restrictDL0008 · matrix_recursive_children_transportDL000C · matrix_recursive_zero_extensionDL0010 · matrix_recursive_cofactor_prefix_from_recursionDL0011 · matrix_recursive_successor_extensionDL0012 · matrix_recursive_all_extensionsDL0013 · signed_recursive_determinant_existsDL0019 · matrix_recursive_lt_add_leftDL001A · matrix_recursive_flattened_index_boundDL001B · matrix_recursive_quotient_row_boundDL0030 · matrix_rank_recode_congruences_existsDL0031 · matrix_rank_bounded_recode_in_fixed_boxDL0032 · matrix_rank_uniform_beta_prefix_box_existsDL003B · matrix_rank_bounded_prefix_decidableDL003E · matrix_rank_selector_dimension_boundDL0053 · matrix_rank_nonzero_minor_dimension_boundsDL005A · matrix_rank_le_successor_casesDL005B · matrix_rank_maximal_nonzero_prefix_existsDL005E · rectangular_matrix_rank_certificate_existsDL0085 · matrix_integer_vector_equality_restrictDL0095 · matrix_integer_rectangular_index_boundDL00A0 · matrix_lattice_absolute_difference_exists