Commit 2024-02-28 16:59 a6f77074

View on Github →

chore: use lt_add_one to simplify proof of exists_abs_lt (#11046)

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Abs.lean

modified theorem exists_abs_lt