4 commits

Author	SHA1	Message	Date
Kim Morrison	10bfeba2d9	chore: aligning Int.ediv/fdiv/tdiv theorems (#7266) ... This PR begins the alignment of `Int.ediv/fdiv/tdiv` theorems.	2025-02-28 05:27:40 +00:00
Kim Morrison	27e1391e6d	feat: complete comparison theorems for ediv/tdiv/fdiv and emod/tmod/fmod (#7199) ... This PR adds theorems comparing `Int.ediv` with `tdiv` and `fdiv`, for all signs of arguments. (Previously we just had the statements about the cases in which they agree.)	2025-02-24 01:01:40 +00:00
Kim Morrison	6c609028b3	feat: upgrade Int.tdiv_eq_ediv to an unconditional equivalence (#7163) ... This PR gives an unconditional theorem expressing `Int.tdiv` in terms of `Int.ediv`, not just for non-negative arguments.	2025-02-20 23:46:11 +00:00
Kim Morrison	2eb478787f	chore: split Int.DivModLemmas into Bootstrap and Lemmas (#7162) ... This PR splits `Int.DivModLemmas` into a `Bootstrap` and `Lemmas` file, where it is possible to use `omega` in `Lemmas`. I'm going to add more theory, particularly about `fdiv` and `tdiv` to the `Lemmas` file, and would prefer to have access to `omega`.	2025-02-20 12:05:09 +00:00