Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Readable signature
Prime(p)Exact expansion
~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.
Definition neighborhood
Depends on conservative definitions
none
Used by conservative definitions
none
All transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
LU0000 lucas_digit_carry_implies_prime_divides LU0001 lucas_prime_row_interior_divisible LU0002 lucas_choose_prime_divisor_bound LU0003 lucas_digit_carry_iff_prime_divides LU0004 lucas_digit_no_carry_iff_not_divides LU0006 lucas_prime_base_digit_total LU000B lucas_prime_base_digit_prefix_exists LU000E lucas_prime_base_two_digit_total LU000I lucas_prime_row_sparse_complete LU000M lucas_prime_block_digit_congruence LU000N lucas_one_step_division_congruence LU000T lucas_prime_row_interior_zero_mod LU000W lucas_prime_shift_below_base LU000X lucas_prime_plus_index_nonzero LU000Z lucas_prime_shift_high_column LU0012 lucas_repeated_prime_shift_below_base LU0014 lucas_low_digit_product_congruence LU001A lucas_prime_digit_chain_exists LU001J lucas_terminating_multidigit_theorem_from_one_step LU001K lucas_prime_digit_nonzero_quotient_strict LU001L lucas_prime_digit_chain_nonzero_index_bound LU001M lucas_prime_digit_chain_terminal_zero LU001N lucas_terminating_prime_digit_chain_exists LU001O lucas_multidigit_congruence LU001P lucas_terminating_multidigit_theorem LU001Q lucas_theorem_for_length LU001R lucas_theoremGrand-campaign planning vocabulary
Locate Prime in the global campaign vocabulary →
Reviewed Prime corresponds to blueprint Prime with checked argument positions [0].
The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.