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 x ≤ S (S i · c) ∧ (∃ y. b = y · S (S i · c) + x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))The 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)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)FpRepresentedDegree(p,b,c,L,d)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)FpMonic(p,b,c,L)FpMonicNormalization(p,k,ab,ac,bb,bc,L)PolynomialLeftPad(b,c,L,t,d,e)PolynomialPowerCoefficient(b,c,L,k,a)FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q)FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)PolynomialShift(b,c,L,d,e)
Checked theorems using this definition
PG0001 · prime_field_polynomial_shift_existsPG0002 · prime_field_polynomial_shift_boundedPG0003 · prime_field_polynomial_shift_functionalPG0008 · prime_field_convolution_coefficient_shift_right_iffPG000A · prime_field_polynomial_convolution_shift_right_nonemptyPG0010 · beta_sum_pointwise_mod_scalePG0011 · polynomial_zero_extended_scale_congruentPG0015 · prime_field_polynomial_convolution_right_scalePG0018 · prime_field_polynomial_scale_zero_valuePG001A · prime_field_polynomial_append_shift_constant_addPG001B · prime_field_polynomial_append_shift_constant_decomposition_existsPG001C · prime_field_convolution_coefficient_right_append_addPG001E · prime_field_polynomial_convolution_right_append_equivalentPG001F · prime_field_polynomial_convolution_right_append_existsPG0023 · prime_field_polynomial_convolution_associativity_append_stepPG0025 · prime_field_polynomial_convolution_associative_equivalentPG002D · polynomial_diagonal_left_unit_first_termPG002F · polynomial_diagonal_left_unit_natural_sumPG0030 · prime_field_convolution_coefficient_left_unitPG0031 · prime_field_polynomial_convolution_left_unit_equalPG0032 · prime_field_polynomial_convolution_left_unit_equivalentPG0033 · prime_field_polynomial_convolution_left_unit_existsPG0034 · prime_field_polynomial_right_divides_reflexivePG004D · 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_scalePG0051 · prime_field_polynomial_scale_to_left_constant_productPG0052 · prime_field_polynomial_left_constant_product_existsPG0055 · prime_field_polynomial_scale_implies_right_dividesPG006D · prime_field_polynomial_nonzero_leading_equivalent_length_boundPG0072 · prime_field_polynomial_monic_singleton_multiple_equivalent