Commit 2024-06-15 21:43 a1210a98
View on Github →feat: a * (b - 1) = a * b - a for truncated subtraction (#13826)
... along with the Nat-specialised versions. Also add a few simple lemmas about div and dvd, restore Nat.mul_div_mul_comm and fix the name AddGroup.toHasOrderedSub to AddGroup.toOrderedSub.
From LeanCamCombi