Vlad Tsyrklevich 78ed072ab0 feat: add Int.emod_sub_emod and Int.sub_emod_emod (#6507) ... This PR adds the subtraction equivalents for `Int.emod_add_emod` (`(a % n + b) % n = (a + b) % n`) and `Int.add_emod_emod` (`(a + b % n) % n = (a + b) % n`). These are marked @[simp] like their addition equivalents. Discussed on Zulip in https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Adding.20some.20sub_emod.20lemmas.20to.20DivModLemmas		2025-01-08 02:20:43 +00:00
..
Bitwise	feat: BitVec.toFin/ToInt BitVec.ushiftRight (#6238)	2024-12-04 01:49:58 +00:00
Basic.lean	feat: lemmas about Std.Range (#6396)	2024-12-16 03:16:46 +00:00
Bitwise.lean	chore: upstream Std.BitVec.* (#3400)	2024-02-19 12:43:34 -08:00
DivMod.lean	chore: remove deprecated aliases for Int.tdiv and Int.tmod (#6322)	2024-12-08 05:19:42 +00:00
DivModLemmas.lean	feat: add Int.emod_sub_emod and Int.sub_emod_emod (#6507)	2025-01-08 02:20:43 +00:00
Gcd.lean	chore: upstream Std.Data.Int (#3635)	2024-03-11 21:40:48 +00:00
Lemmas.lean	chore: fix naming of left/right injectivity lemmas (#6106)	2024-11-18 00:53:46 +00:00
LemmasAux.lean	chore: reverse direction of Int.toNat_sub (#5208)	2024-08-30 02:25:53 +00:00
Order.lean	feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax (#5932)	2024-11-03 16:23:37 +00:00
Pow.lean	chore: restore broken proofs	2024-12-03 17:59:23 +11:00