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 notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
none
Used by definitions
Used by theorem statements or local proof propositions
PA0003 prime_divisor_eq_one_or_self PA0031 prime_nonzero PA0038 euclid_prime_dvd_product PA003M prime_coprime_or_divides PA003N prime_not_divides_coprime PA003S prime_mod_cancel PA0061 prime_is_succ_succ PA0062 prime_mod_inverse PA0063 prime_bounded_nonzero_mod_inverse PA0064 prime_ne_two_is_odd PA006V distinct_primes_left_not_divide_right PA006W distinct_primes_right_not_divide_left PA006X distinct_primes_mutually_nondivisible PA0072 gauss_half_range_signed_choices PA0075 gauss_half_range_signed_prefix_exists PA0079 prime_scaled_same_target_unique PA007A gauss_same_sign_scaled_source_unique PA007B gauss_mixed_sign_scaled_source_impossible PA007C gauss_signed_half_magnitude_injective PA0082 prime_positive_bounded_product_coprime PA0083 prime_half_range_product_coprime PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA008B prime_mul_index_map_exists_up_to PA008E prime_mul_index_map_injective PA008I prime_mul_residue_reindex_exists PA008J prime_mul_residue_product_balance PA008K prime_range_product_coprime PA008L fermat_predecessor_exponent_mod_one PA008M quadratic_residue_half_power_mod_one PA008P prime_scaled_inverse_target_nonzero PA008Q prime_scaled_inverse_exists PA008R prime_scaled_inverse_prefix_extend PA008S prime_scaled_inverse_prefix_exists_bounded PA008T prime_scaled_inverse_prefix_exists PA009C prime_scaled_inverse_unique PA009D scaled_inverse_prefix_extensional PA009E scaled_inverse_prefix_involutive PA009I scaled_inverse_prefix_choose_omitted_orbit PA009O scaled_inverse_pair_order_choose_append PA009T scaled_inverse_pair_order_paired_state_step PA009V scaled_inverse_pair_order_paired_iteration PA009W scaled_inverse_pair_order_terminal_package PA00A2 prime_two_or_terminal_odd_shape PA00A4 prime_inverse_index_exists PA00A5 prime_inverse_prefix_extend PA00A6 prime_inverse_prefix_exists_bounded PA00A7 prime_inverse_prefix_exists PA00AG prime_bounded_square_one_cases PA00AH prime_inverse_prefix_fixed_cases PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AR prime_choose_unused_nonendpoint_orbit PA00AV prime_pair_order_choose_append PA00AW prime_pair_order_choose_append_injective PA00AX prime_pair_order_choose_append_state PA00B0 prime_pair_order_paired_state_step PA00B1 prime_pair_order_paired_iteration PA00B2 prime_pair_order_paired_terminal_state_exists PA00BE prime_wilson_terminal_product_package_exists PA00BF prime_terminal_range_two_product_mod_one_exists PA00BJ prime_factorial_wilson_congruence PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor PA00BM quadratic_nonresidue_half_power_mod_predecessor PA00BN bounded_euler_criterion_dichotomy PA00BP odd_prime_one_not_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BU arbitrary_euler_criterion_complete PA00BV arbitrary_gauss_lemma_complete PA00C0 prime_scaled_half_division_prefix_exists PA00C1 prime_scaled_half_quotient_sum_exists PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00D8 distinct_odd_prime_half_products_ne PA00D9 distinct_odd_prime_half_cell_oriented PA00DA distinct_odd_prime_half_cell_indicator_choice PA00DB distinct_odd_prime_half_row_indicator_choices PA00DF distinct_odd_prime_half_row_count_exists PA00DG distinct_odd_prime_half_row_count_choice PA00DH distinct_odd_prime_half_row_count_choices_bounded PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded PA00DL distinct_odd_prime_half_row_count_prefix_exists PA00DM distinct_odd_prime_half_rectangle_total_exists PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero PA00DO distinct_primes_bounded_scaled_remainder_nonzero PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient PA00E2 distinct_odd_prime_semantic_row_equals_decoded_quotient PA00E3 distinct_odd_prime_quotient_entry_matches_rectangle PA00E4 distinct_odd_prime_quotient_sum_transports_to_rectangle PA00E5 distinct_odd_prime_quotient_sum_equals_rectangle_total PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FW quadratic_reciprocity_combined