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
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
DivRem(n,d,q,r)BoundedNonzeroInverse(m,a)FpElement(p,a)CanonicalModularResidue(m,a,r)FpAdd(p,a,b,c)FpMul(p,a,b,c)FpFieldLaws(p)FpZeroExtendedInv(p,a,b)FpAddPrefix(p,b,c,l)FpMulPrefix(p,b,c,l)FpNegPrefix(p,b,c,l)FpInvPrefix(p,b,c,l)IdentityMatrixSelector(b,c,l)FpCardinality(p,b,c)FpUnitSteps(p,b,c,n)FpCharacteristic(p)
Checked theorems using this definition
FP0002 · prime_field_zero_below_primeFP0003 · prime_field_residue_reflexiveFP0006 · prime_field_residue_bounded_valueFP0008 · prime_field_add_existsFP000A · prime_field_add_exists_uniqueFP000C · prime_field_multiply_existsFP000E · prime_field_multiply_exists_uniqueFP0014 · prime_field_add_zero_rightFP0015 · prime_field_add_zero_leftFP0016 · prime_field_multiply_one_rightFP0017 · prime_field_multiply_one_leftFP0018 · prime_field_multiply_zero_rightFP0019 · prime_field_multiply_zero_leftFP001B · prime_field_negate_existsFP001D · prime_field_negate_exists_uniqueFP001E · prime_field_inverse_existsFP0020 · prime_field_inverse_exists_uniqueFP0024 · prime_field_nonzero_coprimeFP0029 · prime_field_positive_below_modulus_not_zeroFP002B · prime_field_add_grid_value_existsFP002C · prime_field_multiply_grid_value_existsFP002D · prime_field_zero_extended_inverse_existsFP002F · prime_field_add_prefix_choiceFP0030 · prime_field_multiply_prefix_choiceFP0031 · prime_field_negate_prefix_choiceFP0032 · prime_field_inverse_prefix_choiceFP0038 · prime_field_add_grid_value_lookupFP0039 · prime_field_add_table_lookupFP003B · prime_field_multiply_grid_value_lookupFP003C · prime_field_multiply_table_lookupFP003E · prime_field_negate_table_lookupFP0040 · prime_field_inverse_table_lookupFP0042 · prime_field_add_table_commutativeFP0043 · prime_field_add_table_associativeFP0044 · prime_field_multiply_table_commutativeFP0045 · prime_field_multiply_table_associativeFP0046 · prime_field_inverse_table_zeroFP0047 · prime_field_inverse_table_nonzeroFP0048 · prime_field_left_table_distributiveFP0049 · prime_field_right_table_distributiveFP004A · prime_field_enumeration_valueFP004D · prime_field_unit_trace_recodeFP004E · prime_field_unit_trace_successorFP0050 · prime_field_unit_trace_result_boundedFP0051 · prime_field_unit_trace_exists