Commit 2024-12-10 02:59 078c1ad7

View on Github →

feat: more Int.ediv lemmas (#19754)

Estimated changes

Modified Mathlib/Algebra/Order/Group/Unbundled/Int.lean

added theorem Int.sign_mul_self_eq_abs

Modified Mathlib/Data/Int/Defs.lean

added theorem Int.sign_mul_self_eq_natAbs

Modified Mathlib/Data/Int/Lemmas.lean

added theorem Int.ediv_emod_unique'