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
¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1The 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
none
Checked theorems using this definition
PG0002 · prime_field_polynomial_shift_boundedPG000D · prime_field_polynomial_convolution_shift_right_existsPG001A · prime_field_polynomial_append_shift_constant_addPG001B · prime_field_polynomial_append_shift_constant_decomposition_existsPG001C · prime_field_convolution_coefficient_right_append_addPG001D · prime_field_polynomial_shift_scale_aligned_sum_existsPG001E · prime_field_polynomial_convolution_right_append_equivalentPG001F · prime_field_polynomial_convolution_right_append_existsPG0021 · prime_field_polynomial_convolution_shift_scale_aligned_equivalentPG0022 · prime_field_polynomial_shift_scale_aligned_congruentPG0023 · prime_field_polynomial_convolution_associativity_append_stepPG0025 · prime_field_polynomial_convolution_associative_equivalentPG002C · prime_field_polynomial_right_divides_transitivePG0033 · prime_field_polynomial_convolution_left_unit_existsPG0034 · prime_field_polynomial_right_divides_reflexivePG0035 · prime_field_polynomial_bounded_representative_at_length_existsPG0038 · prime_field_polynomial_common_representatives_at_length_existsPG0039 · prime_field_polynomial_common_representatives_existsPG0041 · prime_field_polynomial_aligned_add_functionalPG0042 · prime_field_polynomial_aligned_add_existsPG0043 · prime_field_polynomial_aligned_add_realizePG0045 · prime_field_polynomial_aligned_subtract_existsPG0046 · prime_field_polynomial_aligned_add_cancel_leftPG0047 · prime_field_polynomial_aligned_add_associativePG0048 · prime_field_polynomial_aligned_subtract_functionalPG004A · prime_field_polynomial_division_execution_aligned_identityPG004B · prime_field_polynomial_aligned_convolution_left_addPG004C · prime_field_polynomial_aligned_convolution_right_addPG0051 · prime_field_polynomial_scale_to_left_constant_productPG0052 · prime_field_polynomial_left_constant_product_existsPG0053 · prime_field_polynomial_division_remainder_length_descentPG0054 · prime_field_polynomial_division_constant_remainder_emptyPG0055 · prime_field_polynomial_scale_implies_right_dividesPG0056 · prime_field_polynomial_monic_normalization_right_associatesPG0057 · prime_field_polynomial_normalized_right_associate_existsPG0058 · prime_field_polynomial_right_divides_aligned_addPG0059 · prime_field_polynomial_right_divides_aligned_subtractPG005A · prime_field_polynomial_right_divides_left_productPG005B · prime_field_polynomial_common_right_divisor_euclidean_transportPG005C · prime_field_polynomial_division_execution_common_right_divisorsPG005D · prime_field_polynomial_euclidean_backward_coefficient_identityPG005E · prime_field_polynomial_bezout_euclidean_backwardPG005F · prime_field_polynomial_division_execution_bezout_backwardPG0060 · prime_field_polynomial_aligned_add_empty_rightPG0061 · prime_field_polynomial_bezout_from_right_multiplePG0063 · prime_field_polynomial_bezout_common_right_divisorPG0066 · 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_existsPG006B · prime_field_polynomial_bezout_is_right_gcdPG006C · prime_field_polynomial_normalized_gcd_bezout_existsPG0070 · prime_field_polynomial_right_divides_represented_factorizationPG0071 · prime_field_polynomial_right_divides_represented_degree_boundPG0072 · prime_field_polynomial_monic_singleton_multiple_equivalentPG0073 · prime_field_polynomial_monic_equal_degree_right_divides_equivalentPG0074 · prime_field_polynomial_monic_right_associates_equivalentPG0076 · prime_field_polynomial_normal_right_associates_equivalentPG0077 · prime_field_polynomial_normalized_gcd_equivalent_unique