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
ModularSetMember(b,c,p,x)ModularSetSubset(b,c,d,e,p)ModularSetUnion(b,c,d,e,u,v,p)ModularSetIntersection(b,c,d,e,u,v,p)ModularSetPullback(b,c,d,e,p,t)ModularSetSumCover(b,c,d,e,u,v,p)ModularSetSum(b,c,d,e,u,v,p)ModularTranslationBoundary(b,c,p,d,a,r)ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t)Sum(b,c,l,z)AllBits(b,c,l)
Checked theorems using this definition
CD0001 · finite_bit_entry_casesCD0002 · finite_bit_membership_decidableCD0003 · finite_bit_count_positive_memberCD0004 · finite_bit_subset_pointwise_leCD0007 · finite_add_lt_of_lt_of_leCD0008 · finite_add_lt_of_le_of_ltCD0009 · finite_sum_entry_leCD000B · finite_sum_pointwise_strict_atCD000C · finite_bit_count_proper_subset_ltCD000D · finite_bit_count_missing_zeroCD000E · finite_bit_count_two_nonzero_memberCD000F · finite_sum_pointwise_balanceCD0011 · finite_bit_intersection_from_productCD0012 · finite_bit_intersection_existsCD0013 · finite_bit_complement_existsCD0014 · finite_bit_complement_member_iffCD0015 · finite_bit_union_of_complementsCD0016 · finite_bit_union_existsCD0019 · finite_bit_nonmember_zeroCD001C · finite_beta_composition_existsCD001D · finite_modular_translation_indices_existsCD001E · finite_modular_translation_index_entryCD001F · finite_modular_translation_indices_permutationCD0020 · finite_modular_composition_all_bitsCD0021 · finite_modular_composition_pullbackCD0022 · finite_modular_set_pullback_existsCD0024 · finite_modular_residue_existsCD0025 · finite_modular_additive_complementCD0027 · finite_modular_pullback_membership_witnessCD0028 · finite_modular_pushforward_membership_witnessCD002C · finite_partial_sumset_emptyCD002D · finite_partial_sumset_succ_absentCD002E · finite_partial_sumset_succ_presentCD002F · finite_modular_sumset_prefix_existsCD0030 · finite_modular_sumset_existsCD0033 · prime_modular_additive_orbit_hitsCD0034 · finite_modular_orbit_member_or_boundaryCD0035 · prime_modular_set_translation_boundary_existsCD0036 · finite_modular_dyson_upper_from_unionCD0037 · finite_modular_dyson_lower_from_pullbackCD0038 · finite_modular_dyson_transform_existsCD0039 · finite_modular_dyson_upper_memberCD003A · finite_modular_dyson_lower_subsetCD003B · finite_modular_dyson_lower_zero_memberCD003C · finite_modular_dyson_lower_boundary_nonmemberCD003E · finite_modular_dyson_strict_sizesCD0041 · prime_modular_normalized_boundary_existsCD0042 · prime_cauchy_davenport_normalized_bounded_inductionCD0044 · finite_modular_pullback_zero_member