PD0007 · conservative definition

DivRem

q and r are a quotient and a strict remainder for n by d.

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 = d

This 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

PD0002 Lt

Used by conservative definitions

none

All transitive conservative prerequisites

PD0002 Lt

Used by theorem statements or local proof propositions

TS000U affine_grid_point_remainder_exists TS000V beta_affine_residue_grid_extend TS000W beta_affine_residue_grid_exists

Grand-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.