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.
Definition in prerequisite notation
∃ k. n = d · kOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists k. n = d * kThe 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
Checked theorems using this definition
EL000B · lte_nondivisor_nonzeroEL000C · lte_prime_nondivisor_oneEL000D · lte_nondivisor_product_rightEL000E · lte_nondivisor_add_multipleEL000F · lte_prime_nondivisor_twoEL0010 · lte_nondivisor_powerEL0011 · lte_prime_divides_correctionEL0012 · lte_odd_prime_quotient_unitEL0016 · lte_prime_self_valuation_valueEL001A · lte_valuation_from_exact_cofactorEL001B · lte_odd_prime_power_difference_quotientEL001C · lte_coprime_power_difference_quotientEL001D · lte_power_difference_valuation_stepEL001E · lte_odd_prime_power_stepEL001F · lte_coprime_exponent_stepEL0020 · lte_prime_power_iterationEL0021 · lte_positive_exponent_exactEL0024 · odd_prime_lifting_the_exponentEL0026 · odd_prime_lifting_the_exponent_value