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
S a ≤ bOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists h. h + S 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
MatrixSkipIndex(i,r,s)MatrixMinorPrefix(b,c,w,r,d,u,v,q,l)SignedDeterminantChildPrefix(b,c,limit,pb,pc,nb,nc,q,eb,ec,fb,fc,l)SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l)Sum(b,c,l,z)SignedDeterminantHistory(b,c,l)SignedRecursiveDeterminant(pb,pc,nb,nc,d,p,n)SignedEvaluatedCofactors(pb,pc,nb,nc,q,eb,ec,fb,fc)SignedMatrixPrefixEquality(pb,pc,nb,nc,qb,qc,rb,rc,d)UniformBetaPrefixBox(c,T,l,B)FiniteMatrixSelector(b,c,l,B)SignedSelectedSubmatrix(pb,pc,nb,nc,w,rb,rc,cb,cc,q,ub,uc,vb,vc)RectangularMatrixRank(pb,pc,nb,nc,r,w,rank)IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l)IntegerVectorZero(ab,ac,db,dc,l)IntegerVectorAdd(ab,ac,db,dc,eb,ec,fb,fc,pb,pc,nb,nc,l)MatrixAffineSlice(b,c,s,d,u,v,l)DotProduct(b,c,d,e,ell,z)MatrixProductPrefix(lb,lc,rb,rc,w,v,tb,tc,l)MatrixPointwiseAdd(mb,mc,sb,sc,tb,tc,l)IdentityMatrixSelector(b,c,l)
Checked theorems using this definition
DL0002 · matrix_recursive_prefix_reflDL0003 · matrix_recursive_prefix_transDL0004 · matrix_recursive_prefix_restrictDL0005 · matrix_recursive_record_transportDL0006 · matrix_recursive_record_appendDL0008 · matrix_recursive_children_transportDL0009 · matrix_recursive_step_transportDL000A · matrix_recursive_history_transportDL000B · matrix_recursive_history_extendDL000C · matrix_recursive_zero_extensionDL000E · matrix_recursive_children_recodeDL000F · matrix_recursive_children_extendDL0010 · matrix_recursive_cofactor_prefix_from_recursionDL0011 · matrix_recursive_successor_extensionDL0012 · matrix_recursive_all_extensionsDL0013 · signed_recursive_determinant_existsDL0016 · matrix_recursive_history_step_atDL0018 · signed_recursive_determinant_successor_decompositionDL0019 · matrix_recursive_lt_add_leftDL001A · matrix_recursive_flattened_index_boundDL001B · matrix_recursive_quotient_row_boundDL001C · matrix_recursive_minor_cell_transportDL001D · matrix_recursive_minor_prefix_transportDL001E · matrix_recursive_minor_prefix_functionalDL0020 · matrix_recursive_alternating_prefix_transportDL0021 · matrix_recursive_alternating_fold_transportDL0022 · matrix_recursive_alternating_fold_extensionalDL0024 · matrix_recursive_initial_row_prefixDL0025 · matrix_recursive_cofactor_streams_from_functionalityDL0026 · matrix_recursive_determinant_extensionalDL0029 · signed_recursive_determinant_from_evaluated_cofactorsDL002B · signed_recursive_determinant_emptyDL002D · matrix_rank_bounded_prefix_valueDL002E · matrix_rank_common_multiple_dividesDL002F · matrix_rank_beta_moduli_common_multipleDL0030 · matrix_rank_recode_congruences_existsDL0031 · matrix_rank_bounded_recode_in_fixed_boxDL0033 · matrix_rank_no_index_below_zeroDL0034 · matrix_rank_prefix_equality_symmetricDL0035 · matrix_rank_bounded_prefix_transportDL0036 · matrix_rank_injective_prefix_transportDL0037 · matrix_rank_injective_prefix_decidableDL0038 · matrix_rank_bounded_prefix_emptyDL0039 · matrix_rank_bounded_prefix_drop_lastDL003A · matrix_rank_bounded_prefix_extendDL003B · matrix_rank_bounded_prefix_decidableDL003C · matrix_rank_selector_transportDL003D · matrix_rank_selector_decidableDL003E · matrix_rank_selector_dimension_boundDL0040 · matrix_rank_selected_point_existsDL0041 · matrix_rank_selected_point_functionalDL0042 · matrix_rank_selected_prefix_emptyDL0043 · matrix_rank_selected_prefix_extendDL0044 · matrix_rank_selected_prefix_exists_nonzeroDL0045 · matrix_rank_selected_square_existsDL0046 · matrix_rank_signed_selected_square_existsDL0047 · matrix_rank_selected_prefix_functionalDL004B · matrix_rank_selected_point_selector_transportDL004C · matrix_rank_selected_prefix_selector_transportDL004D · matrix_rank_signed_selected_selector_transportDL004E · matrix_rank_selected_determinant_selector_transportDL0051 · matrix_rank_nonzero_selected_minor_transportDL0055 · matrix_rank_selected_column_search_decidableDL0056 · matrix_rank_selected_box_search_decidableDL0057 · matrix_rank_nonzero_minor_recode_in_boxDL0058 · matrix_rank_nonzero_minor_of_box_searchDL0059 · matrix_rank_nonzero_minor_decidableDL005A · matrix_rank_le_successor_casesDL005B · matrix_rank_maximal_nonzero_prefix_existsDL005E · rectangular_matrix_rank_certificate_existsDL0064 · integer_span_dot_product_pointwise_addDL0066 · integer_span_natural_product_entryDL008E · matrix_integer_minor_cell_balanceDL008F · matrix_integer_minor_prefix_cell_at_coordinatesDL0090 · matrix_integer_square_index_width_nonzeroDL0091 · matrix_integer_signed_minor_balanceDL0095 · matrix_integer_rectangular_index_boundDL0096 · matrix_integer_selected_point_at_sourceDL0097 · matrix_integer_selected_point_balanceDL0098 · matrix_integer_selected_prefix_point_atDL00AE · matrix_lattice_identity_selector_existsDL00B0 · matrix_lattice_identity_selected_natural