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
PQ002E · prime_field_polynomial_trim_represented_degreePQ002F · prime_field_polynomial_trim_nonempty_degree_existsPQ0030 · prime_field_polynomial_trim_represented_identityPQ0032 · prime_field_polynomial_monic_represented_degreePQ003B · prime_field_polynomial_monic_normalization_represented_degreePQ003C · prime_field_polynomial_monic_normalization_existsPQ0043 · prime_field_polynomial_monic_normalization_exists_uniquePQ0044 · prime_field_polynomial_monic_normalization_degree_zero_existsPQ0052 · prime_field_polynomial_synthetic_represented_degree