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
DivRem(n, d, q, r)Exact expansion
n = d * q + r /\ exists h. h + S r = dThis 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
Used by conservative definitions
All transitive conservative prerequisites
Used by theorem statements or local proof propositions
LU0005 lucas_base_p_digit_total LU0006 lucas_prime_base_digit_total LU0007 lucas_base_p_digit_functional LU0008 lucas_base_p_digit_of_small_value LU0009 lucas_base_p_zero_digit_iff_divides LU000C lucas_base_p_digit_prefix_point LU000D lucas_base_p_two_digit_total LU000E lucas_prime_base_two_digit_total LU000F lucas_base_p_two_digit_reconstruction LU0016 lucas_digit_chain_empty LU0017 lucas_digit_chain_empty_exists LU0018 lucas_digit_chain_extend LU0019 lucas_digit_chain_exists LU001A lucas_prime_digit_chain_exists LU001B lucas_digit_chain_initial_value LU001C lucas_digit_chain_step_exists LU001I lucas_multidigit_congruence_from_one_step LU001J lucas_terminating_multidigit_theorem_from_one_step 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 DivRem in the global campaign vocabulary →
Reviewed DivRem corresponds to blueprint DivRem with checked argument positions [0, 1, 2, 3].
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.