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
PQ0001 · prime_field_subtract_existsPQ0002 · prime_field_subtract_equal_zeroPQ0004 · prime_field_polynomial_negate_existsPQ000A · prime_field_polynomial_negate_zeroPQ000D · prime_field_polynomial_subtract_existsPQ0014 · prime_field_polynomial_subtract_self_zeroPQ0015 · prime_field_polynomial_subtract_zero_rightPQ0017 · prime_field_polynomial_subtract_equal_entry_zeroPQ0018 · prime_field_polynomial_subtract_equal_zeroPQ0036 · prime_field_polynomial_monic_normalization_scalar_nonzeroPQ003C · prime_field_polynomial_monic_normalization_existsPQ0041 · prime_field_polynomial_monic_normalization_fixedPQ0043 · prime_field_polynomial_monic_normalization_exists_uniquePQ0044 · prime_field_polynomial_monic_normalization_degree_zero_existsPQ0046 · prime_field_polynomial_horner_trace_state_boundedPQ0047 · prime_field_polynomial_synthetic_existsPQ004A · prime_field_polynomial_synthetic_quotient_boundedPQ004B · prime_field_polynomial_synthetic_remainder_boundedPQ004C · prime_field_polynomial_synthetic_functionalPQ004D · prime_field_polynomial_horner_constant_valuePQ004E · prime_field_polynomial_horner_transition_valuesPQ004F · prime_field_polynomial_synthetic_leading_coefficientPQ0050 · prime_field_polynomial_synthetic_middle_coefficientsPQ0051 · prime_field_polynomial_synthetic_final_coefficientPQ0052 · prime_field_polynomial_synthetic_represented_degreePQ0053 · prime_field_polynomial_synthetic_constantPQ0054 · prime_field_polynomial_synthetic_exists_uniquePQ0055 · prime_field_polynomial_synthetic_zero_remainder_iff