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
Dvd(d,n)Exact expansion
exists k. n = d * kThis 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 PA000C multiple_mul_right PA000I bounded_common_multiple_step PA000K bounded_common_multiple_exists PA000L scaled_bounded_common_multiple PA000O divisor_one PA000T right_factor_divides_product PA0013 factor_difference PA0014 divides_remainder PA0015 beta_modulus_coprime_base PA0017 common_divisor_beta_moduli_divides_gap_times_c PA0018 multiple_trans PA0019 multiple_refl PA001E multiple_zero PA001G divides_linear_step PA001O common_divisor_divides_balanced_result PA001P gauss_coprime_cancel PA001Q beta_moduli_coprime_of_gap_dvd PA001R beta_moduli_coprime_of_lt_bounded_common_multiple PA001S beta_moduli_pairwise_coprime_bounded PA001T coprime_mul_left PA001U beta_exclusive_accumulated_product_step PA0021 dvd_to_mod_zero PA0027 mod_eq_of_mod_eq_multiple PA0028 binary_crt_fold_step PA002G beta_exclusive_recode_congruence_step PA002H beta_exclusive_recode_invariant_step PA002I bounded_beta_exclusive_recode_invariant PA002X beta_prefix_extend PA0037 is_gcd_one_to_coprime PA0038 euclid_prime_dvd_product PA0039 divisor_le_nonzero PA003M prime_coprime_or_divides PA003N prime_not_divides_coprime PA003S prime_mod_cancel PA0062 prime_mod_inverse PA0063 prime_bounded_nonzero_mod_inverse 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 PA0085 gauss_lemma_power_congruence_exists PA0086 nondivisor_canonical_remainder_exists PA0089 bounded_nonzero_not_divides PA008A mod_eq_zero_to_dvd_nonzero 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 PA009C prime_scaled_inverse_unique PA00AG prime_bounded_square_one_cases PA00BN bounded_euler_criterion_dichotomy PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BU arbitrary_euler_criterion_complete PA00BV arbitrary_gauss_lemma_complete 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 PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero PA00DO distinct_primes_bounded_scaled_remainder_nonzero PA00FG distinct_odd_primes_gauss_eisenstein_data_exists