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
Sum(b,c,l,z)Repeat(b,c,a,l)CanonicalModularResidue(m,a,r)FpAdd(p,a,b,c)FpMul(p,a,b,c)BetaPrefixInto(b,c,l,B)BetaPrefixEqual(b,c,d,e,l)FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)FpPolyScale(p,k,ab,ac,bb,bc,l)BetaZeroExtend(b,c,L,i,a)PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l)FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,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)PolynomialLeftPad(b,c,L,t,d,e)FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)
Checked theorems using this definition
PG0002 · prime_field_polynomial_shift_boundedPG0003 · prime_field_polynomial_shift_functionalPG0004 · prime_field_polynomial_shift_zero_prefixPG0005 · polynomial_zero_extended_shift_forwardPG0010 · beta_sum_pointwise_mod_scalePG0017 · prime_field_polynomial_convolution_right_scale_existsPG001A · prime_field_polynomial_append_shift_constant_addPG001B · prime_field_polynomial_append_shift_constant_decomposition_existsPG001C · prime_field_convolution_coefficient_right_append_addPG001D · prime_field_polynomial_shift_scale_aligned_sum_existsPG001F · prime_field_polynomial_convolution_right_append_existsPG0023 · prime_field_polynomial_convolution_associativity_append_stepPG002D · polynomial_diagonal_left_unit_first_termPG002E · polynomial_diagonal_left_unit_tail_termPG002F · polynomial_diagonal_left_unit_natural_sumPG0030 · prime_field_convolution_coefficient_left_unitPG004D · polynomial_diagonal_left_constant_first_termPG004E · polynomial_diagonal_left_constant_natural_sumPG004F · prime_field_convolution_coefficient_left_constantPG0050 · prime_field_polynomial_left_constant_product_to_scalePG0052 · prime_field_polynomial_left_constant_product_existsPG0053 · prime_field_polynomial_division_remainder_length_descentPG0054 · prime_field_polynomial_division_constant_remainder_emptyPG0069 · prime_field_polynomial_gcd_bezout_exists_up_toPG006D · prime_field_polynomial_nonzero_leading_equivalent_length_boundPG006F · prime_field_polynomial_product_equivalent_nonzero_left_nonempty