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
Repeat(b,c,a,l)BetaPrefixInto(b,c,l,B)FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)FpPolyScale(p,k,ab,ac,bb,bc,l)FpHornerStep(p,b,c,x,u,v,i)FpHornerTrace(p,b,c,x,l,r,u,v)FpRepresentedDegree(p,b,c,L,d)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)FpMonic(p,b,c,L)FpMonicNormalization(p,k,ab,ac,bb,bc,L)
Checked theorems using this definition
PQ0004 · prime_field_polynomial_negate_existsPQ0005 · prime_field_polynomial_negate_entryPQ0006 · prime_field_polynomial_negate_boundedPQ0007 · prime_field_polynomial_negate_functionalPQ0008 · prime_field_polynomial_negate_transportPQ0009 · prime_field_polynomial_negate_involutivePQ000B · prime_field_polynomial_negate_add_zeroPQ000D · prime_field_polynomial_subtract_existsPQ000E · prime_field_polynomial_subtract_entryPQ000F · prime_field_polynomial_subtract_boundedPQ0010 · prime_field_polynomial_subtract_functionalPQ0011 · prime_field_polynomial_subtract_transportPQ0012 · prime_field_polynomial_subtract_recover_addPQ0013 · prime_field_polynomial_subtract_from_addPQ0017 · 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_cancelPQ001B · prime_field_polynomial_suffix_existsPQ001C · prime_field_polynomial_suffix_entryPQ001D · prime_field_polynomial_suffix_boundedPQ001E · prime_field_polynomial_suffix_equalPQ001F · prime_field_polynomial_leading_zero_cut_existsPQ0020 · prime_field_polynomial_trim_from_cutPQ0021 · prime_field_polynomial_trim_existsPQ0025 · prime_field_polynomial_trim_leading_source_nonzeroPQ0027 · prime_field_polynomial_trim_empty_of_zeroPQ0029 · prime_field_polynomial_trim_removed_lePQ002C · prime_field_polynomial_trim_output_equalPQ002D · prime_field_polynomial_trim_exists_uniquePQ0031 · prime_field_polynomial_monic_leading_valuePQ0033 · prime_field_polynomial_monic_transportPQ0035 · prime_field_polynomial_monic_normalization_inversePQ0037 · prime_field_polynomial_monic_normalization_entryPQ0039 · prime_field_polynomial_monic_normalization_leadingPQ003E · 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_uniquePQ0045 · prime_field_polynomial_horner_trace_prefixPQ0046 · prime_field_polynomial_horner_trace_state_boundedPQ0049 · prime_field_polynomial_synthetic_quotient_entryPQ004A · prime_field_polynomial_synthetic_quotient_boundedPQ004C · prime_field_polynomial_synthetic_functionalPQ004D · prime_field_polynomial_horner_constant_valuePQ004E · prime_field_polynomial_horner_transition_valuesPQ004F · prime_field_polynomial_synthetic_leading_coefficientPQ0050 · prime_field_polynomial_synthetic_middle_coefficientsPQ0051 · prime_field_polynomial_synthetic_final_coefficientPQ0053 · prime_field_polynomial_synthetic_constantPQ0054 · prime_field_polynomial_synthetic_exists_unique