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
G = 0 ∨ FpMonic(p,gb,gc,G)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(G)=0 \/ (((~((G) = 0)) /\ (((forall fom_index_pfp_gcd_definition_normal_moniccoefficients. (exists fom_gap_pfp_gcd_definition_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_definition_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_definition_normal_moniccoefficients) = G) -> exists fom_value_pfp_gcd_definition_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_definition_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_definition_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_definition_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_definition_normal_moniccoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_definition_normal_moniccoefficients_entry. gb = fom_beta_quotient_pfp_gcd_definition_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_definition_normal_moniccoefficients)) * gc) + (fom_value_pfp_gcd_definition_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_definition_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_definition_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_definition_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_definition_normal_monicleading. ff_h_pfp_gcd_definition_normal_monicleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_gcd_definition_normal_monicleading. gb = ff_q_pfp_gcd_definition_normal_monicleading * S ((S (0)) * gc) + (1))))))))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
Checked theorems using this definition
PG0057 · prime_field_polynomial_normalized_right_associate_existsPG0066 · prime_field_polynomial_gcd_bezout_empty_secondPG0067 · prime_field_polynomial_gcd_bezout_equivalent_secondPG0068 · prime_field_polynomial_gcd_bezout_division_backwardPG0069 · prime_field_polynomial_gcd_bezout_exists_up_toPG006A · prime_field_polynomial_gcd_bezout_existsPG006C · prime_field_polynomial_normalized_gcd_bezout_existsPG0076 · prime_field_polynomial_normal_right_associates_equivalent