Theorem Int.natAbs_sub_pos_iff

Modification history

2024-08-09 11:40

Mathlib/Algebra/Order/Group/Int.lean

chore (Algebra.Order.Group.Int): split file into unbundled and bundled ordered algebra (#15069) …

Modified Int.natAbs_sub_pos_iff View on Github →

2024-02-23 19:51

Mathlib/Data/Int/Order/Basic.lean

feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027) …

Added Int.natAbs_sub_pos_iff View on Github →