Lemmas about integer division needed to bootstrap omega
. #
dvd #
ediv zero #
emod zero #
ofNat mod #
mod definitions #
@[deprecated Int.emod_add_mul_ediv (since := "2025-09-01")]
Equations
Instances For
@[deprecated Int.emod_add_ediv_mul (since := "2025-09-01")]
Equations
Instances For
@[deprecated Int.mul_ediv_add_emod (since := "2025-09-01")]
Equations
Instances For
@[deprecated Int.ediv_mul_add_emod (since := "2025-09-01")]
Equations
Instances For
/
ediv #
@[reducible, inline, deprecated Int.ediv_nonneg_iff_of_pos (since := "2025-02-28")]