Commit 2025-11-28 17:46 a9158acb

View on Github →

chore(Algebra/Order/Group/Unbundled): golf abs_le_one_iff (+ others) using grind (#32175)

Estimated changes

modified theorem Int.natAbs_abs