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
PX0016 · prime_field_polynomial_left_pad_boundedPX001E · prime_field_polynomial_add_left_pad_transportPX001F · prime_field_polynomial_subtract_left_pad_transportPX0020 · prime_field_polynomial_scale_left_pad_transportPX0023 · prime_field_polynomial_constant_right_coefficientPX0024 · prime_field_polynomial_constant_product_to_scalePX0025 · prime_field_polynomial_scale_to_constant_productPX0026 · prime_field_polynomial_inverse_scalePX0027 · prime_field_polynomial_quotient_scalar_cancellationPX002E · prime_field_polynomial_quotient_prefix_existsPX002F · prime_field_polynomial_quotient_prefix_convolution_entryPX0030 · prime_field_polynomial_quotient_prefix_product_matchesPX0031 · prime_field_polynomial_quotient_prefix_remainder_zeroPX0037 · prime_field_polynomial_division_quotient_data_existsPX0038 · prime_field_polynomial_division_residual_data_existsPX0039 · prime_field_polynomial_division_execution_existsPX003A · prime_field_polynomial_division_remainder_degreePX003B · prime_field_polynomial_division_exists_with_remainder_boundPX003F · prime_field_polynomial_division_coefficient_identityPX005A · prime_field_polynomial_division_execution_exists_uniquePX0071 · prime_field_polynomial_convolution_both_left_paddings_existsPX0073 · prime_field_polynomial_add_left_pad_outputPX0074 · prime_field_polynomial_subtract_left_pad_outputPX0075 · prime_field_polynomial_add_equivalent_congruentPX0076 · prime_field_polynomial_subtract_equivalent_congruent