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
PP000B · prime_field_polynomial_zero_existsPP0013 · prime_field_polynomial_add_zero_rightPP001A · prime_field_polynomial_scale_onePP001B · prime_field_polynomial_scale_zeroPP0020 · prime_field_polynomial_horner_canonical_stepPP0021 · prime_field_polynomial_horner_trace_from_normalizationPP0022 · prime_field_polynomial_horner_existsPP0027 · prime_field_polynomial_horner_normalization_residuePP0028 · prime_field_polynomial_horner_residuePP0029 · prime_field_polynomial_horner_functionalPP002A · prime_field_polynomial_horner_exists_uniquePP002B · prime_field_polynomial_horner_empty_constructPP002C · prime_field_polynomial_horner_successor_constructPP002D · prime_field_polynomial_horner_constantPP002E · prime_field_polynomial_horner_zeroPP002F · prime_field_polynomial_normalized_horner_iffPP0030 · prime_field_polynomial_horner_result_boundedPP0031 · prime_field_polynomial_reduce_and_evaluate_exists