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
L = S d ∧ (BetaPrefixInto(b,c,L,p) ∧ (∃ x. BetaAt(b,c,0,x) ∧ ¬x = 0))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((L))=S ((d))) /\ (((forall fom_index_pfp_lowercontinuationcoefficients. (exists fom_gap_pfp_lowercontinuationcoefficients_index_bound. fom_gap_pfp_lowercontinuationcoefficients_index_bound + S (fom_index_pfp_lowercontinuationcoefficients) = (L)) -> exists fom_value_pfp_lowercontinuationcoefficients. ((((exists fom_beta_height_pfp_lowercontinuationcoefficients_entry. fom_beta_height_pfp_lowercontinuationcoefficients_entry + S (fom_value_pfp_lowercontinuationcoefficients) = S ((S (fom_index_pfp_lowercontinuationcoefficients)) * (c))) /\ exists fom_beta_quotient_pfp_lowercontinuationcoefficients_entry. (b) = fom_beta_quotient_pfp_lowercontinuationcoefficients_entry * S ((S (fom_index_pfp_lowercontinuationcoefficients)) * (c)) + (fom_value_pfp_lowercontinuationcoefficients))) /\ (exists fom_gap_pfp_lowercontinuationcoefficients_value_bound. fom_gap_pfp_lowercontinuationcoefficients_value_bound + S (fom_value_pfp_lowercontinuationcoefficients) = (p)))) /\ ((exists pfd_leading_lowercontinuation. ((((exists ff_h_pfp_lowercontinuationentry. ff_h_pfp_lowercontinuationentry + S (pfd_leading_lowercontinuation) = S ((S (0)) * (c))) /\ exists ff_q_pfp_lowercontinuationentry. (b) = ff_q_pfp_lowercontinuationentry * S ((S (0)) * (c)) + (pfd_leading_lowercontinuation))) /\ ((~(pfd_leading_lowercontinuation=0)))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
PG0053 · prime_field_polynomial_division_remainder_length_descentPG0057 · prime_field_polynomial_normalized_right_associate_existsPG0065 · prime_field_polynomial_reduced_representative_existsPG0069 · prime_field_polynomial_gcd_bezout_exists_up_toPG006E · prime_field_polynomial_equivalent_represented_degrees_equalPG006F · prime_field_polynomial_product_equivalent_nonzero_left_nonemptyPG0070 · prime_field_polynomial_right_divides_represented_factorizationPG0071 · prime_field_polynomial_right_divides_represented_degree_boundPG0073 · prime_field_polynomial_monic_equal_degree_right_divides_equivalentPG0074 · prime_field_polynomial_monic_right_associates_equivalent