PD0004

Prime(p)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

p is nonunit and every factorization of p has a unit factor.

Conservative notation; not a theorem, primitive, or axiom.

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 = 1

The 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

FpElement(p,a)

Checked theorems using this definition

FP0002 · prime_field_zero_below_primeFP0007 · prime_field_residue_modulus_zeroFP0008 · prime_field_add_existsFP000A · prime_field_add_exists_uniqueFP000C · prime_field_multiply_existsFP000E · prime_field_multiply_exists_uniqueFP0014 · prime_field_add_zero_rightFP0015 · prime_field_add_zero_leftFP0016 · prime_field_multiply_one_rightFP0017 · prime_field_multiply_one_leftFP0018 · prime_field_multiply_zero_rightFP0019 · prime_field_multiply_zero_leftFP001B · prime_field_negate_existsFP001D · prime_field_negate_exists_uniqueFP001E · prime_field_inverse_existsFP0020 · prime_field_inverse_exists_uniqueFP0021 · prime_field_zero_has_no_multiplicative_inverseFP0022 · prime_field_inverse_output_nonzeroFP0023 · prime_field_inverse_symmetricFP0024 · prime_field_nonzero_coprimeFP0025 · prime_field_multiply_cancel_nonzero_leftFP0026 · prime_field_no_zero_divisorsFP002A · prime_field_arithmetic_lawsFP002B · prime_field_add_grid_value_existsFP002C · prime_field_multiply_grid_value_existsFP002D · prime_field_zero_extended_inverse_existsFP0033 · prime_field_add_table_existsFP0034 · prime_field_multiply_table_existsFP0035 · prime_field_negate_table_existsFP0036 · prime_field_inverse_table_existsFP0037 · prime_field_operation_tables_existsFP0046 · prime_field_inverse_table_zeroFP004F · prime_field_unit_trace_residueFP0050 · prime_field_unit_trace_result_boundedFP0051 · prime_field_unit_trace_existsFP0052 · prime_field_unit_multiple_residueFP0053 · prime_field_unit_multiple_from_residueFP0054 · prime_field_unit_multiple_functionalFP0055 · prime_field_unit_multiple_exists_uniqueFP0056 · prime_field_characteristic_exactFP0057 · prime_field_of_prime_order_exists