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)Repeat(b,c,a,l)DivisionPrefix(m,b,c,qb,qc,rb,rc,l)BetaPrefixInto(b,c,l,B)BetaPrefixEqual(b,c,d,e,l)Horner(b,c,x,ell,z)CanonicalModularResidue(m,a,r)FpCoefficientReduction(p,b,c,d,e,l)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)
Checked theorems using this definition
PP0003 · prime_field_polynomial_normalization_entryPP0006 · prime_field_polynomial_normalization_reflexivePP0009 · prime_field_polynomial_repeat_coefficientsPP000A · prime_field_polynomial_repeat_existsPP000C · prime_field_polynomial_add_from_normalizationPP000D · prime_field_polynomial_add_existsPP000E · prime_field_polynomial_add_entryPP0013 · prime_field_polynomial_add_zero_rightPP0014 · prime_field_polynomial_scale_from_normalizationPP0015 · prime_field_polynomial_scale_existsPP0016 · prime_field_polynomial_scale_entryPP001A · prime_field_polynomial_scale_onePP001B · prime_field_polynomial_scale_zeroPP0020 · prime_field_polynomial_horner_canonical_stepPP0021 · prime_field_polynomial_horner_trace_from_normalizationPP0022 · prime_field_polynomial_horner_existsPP0023 · prime_field_polynomial_horner_input_boundsPP0027 · prime_field_polynomial_horner_normalization_residuePP0028 · prime_field_polynomial_horner_residuePP002A · prime_field_polynomial_horner_exists_uniquePP002B · prime_field_polynomial_horner_empty_constructPP002C · prime_field_polynomial_horner_successor_constructPP002D · prime_field_polynomial_horner_constantPP002E · prime_field_polynomial_horner_zeroPP002F · prime_field_polynomial_normalized_horner_iffPP0030 · prime_field_polynomial_horner_result_boundedPP0031 · prime_field_polynomial_reduce_and_evaluate_exists