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
Repeat(b,c,a,l)BetaPrefixInto(b,c,l,B)CanonicalModularResidue(m,a,r)FpAdd(p,a,b,c)FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)FpMul(p,a,b,c)FpPolyScale(p,k,ab,ac,bb,bc,l)FpHornerSteps(p,b,c,x,l,u,v)FpHornerTrace(p,b,c,x,l,r,u,v)MatrixAffineSlice(b,c,s,d,u,v,l)FpCoefficientNegation(p,ab,ac,rb,rc,L)FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L)PolynomialSuffix(b,c,t,d,e,M)FpPolynomialTrim(p,b,c,L,t,d,e,M)
Checked theorems using this definition
PQ0001 · prime_field_subtract_existsPQ0004 · prime_field_polynomial_negate_existsPQ0005 · prime_field_polynomial_negate_entryPQ0007 · prime_field_polynomial_negate_functionalPQ0008 · prime_field_polynomial_negate_transportPQ000D · prime_field_polynomial_subtract_existsPQ000E · prime_field_polynomial_subtract_entryPQ0010 · prime_field_polynomial_subtract_functionalPQ0011 · prime_field_polynomial_subtract_transportPQ0017 · prime_field_polynomial_subtract_equal_entry_zeroPQ0018 · prime_field_polynomial_subtract_equal_zeroPQ0019 · prime_field_polynomial_subtract_add_cancelPQ001A · prime_field_polynomial_subtract_common_right_cancelPQ001C · prime_field_polynomial_suffix_entryPQ001D · prime_field_polynomial_suffix_boundedPQ001E · prime_field_polynomial_suffix_equalPQ001F · prime_field_polynomial_leading_zero_cut_existsPQ0027 · prime_field_polynomial_trim_empty_of_zeroPQ0029 · prime_field_polynomial_trim_removed_lePQ002C · prime_field_polynomial_trim_output_equalPQ002D · prime_field_polynomial_trim_exists_uniquePQ0033 · prime_field_polynomial_monic_transportPQ0037 · prime_field_polynomial_monic_normalization_entryPQ0038 · prime_field_polynomial_monic_normalization_boundedPQ0039 · prime_field_polynomial_monic_normalization_leadingPQ003A · prime_field_polynomial_monic_normalization_monicPQ003C · prime_field_polynomial_monic_normalization_existsPQ003E · prime_field_polynomial_monic_normalization_functionalPQ003F · prime_field_polynomial_monic_normalization_value_functionalPQ0040 · prime_field_polynomial_monic_normalization_transportPQ0043 · prime_field_polynomial_monic_normalization_exists_uniquePQ0046 · prime_field_polynomial_horner_trace_state_boundedPQ0047 · prime_field_polynomial_synthetic_existsPQ0049 · prime_field_polynomial_synthetic_quotient_entryPQ004B · prime_field_polynomial_synthetic_remainder_boundedPQ004C · prime_field_polynomial_synthetic_functionalPQ004D · prime_field_polynomial_horner_constant_valuePQ0050 · prime_field_polynomial_synthetic_middle_coefficientsPQ0054 · prime_field_polynomial_synthetic_exists_unique