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)MatrixAffineSlice(b,c,s,d,u,v,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
PX0001 · polynomial_diagonal_left_prefix_transportPX0003 · prime_field_convolution_coefficient_prefix_transportPX0004 · prime_field_convolution_coefficient_append_invariantPX0009 · prime_field_polynomial_power_index_boundPX000A · prime_field_polynomial_left_pad_index_casesPX000B · prime_field_polynomial_power_index_before_paddingPX000C · prime_field_polynomial_power_coefficient_existsPX0014 · prime_field_polynomial_left_pad_existsPX0015 · prime_field_polynomial_left_pad_entryPX0016 · prime_field_polynomial_left_pad_boundedPX0017 · prime_field_polynomial_left_pad_functionalPX001A · prime_field_polynomial_left_pad_power_coefficientPX001E · prime_field_polynomial_add_left_pad_transportPX001F · prime_field_polynomial_subtract_left_pad_transportPX0020 · prime_field_polynomial_scale_left_pad_transportPX0023 · prime_field_polynomial_constant_right_coefficientPX002B · prime_field_polynomial_quotient_prefix_entryPX002D · prime_field_polynomial_quotient_prefix_appendPX002E · prime_field_polynomial_quotient_prefix_existsPX002F · prime_field_polynomial_quotient_prefix_convolution_entryPX0032 · polynomial_quotient_length_existsPX0034 · prime_field_polynomial_trim_zero_prefix_cut_boundPX0036 · prime_field_polynomial_trim_bounded_degreePX0037 · prime_field_polynomial_division_quotient_data_existsPX003A · prime_field_polynomial_division_remainder_degreePX003B · prime_field_polynomial_division_exists_with_remainder_boundPX0040 · beta_sum_pointwise_mod_addPX0054 · prime_field_polynomial_quotient_prefix_functionalPX005C · polynomial_zero_extended_left_pad_beforePX005D · polynomial_left_pad_zero_prefixPX005F · polynomial_zero_tail_natural_sum_invariantPX0062 · polynomial_diagonal_term_left_padding_zero_leftPX0063 · polynomial_diagonal_term_left_padding_zero_rightPX0065 · polynomial_diagonal_left_padding_rightPX0067 · prime_field_convolution_coefficient_left_padding_rightPX0068 · prime_field_convolution_coefficient_before_left_padding_leftPX0069 · prime_field_convolution_coefficient_before_left_padding_right