Theorem Int.natAbs_add_of_nonpos

Modification history

2024-04-08 09:07

Mathlib/Data/Int/Defs.lean

chore: replace proof of natAbs_add_of_nonpos (#11995) …

Modified Int.natAbs_add_of_nonpos View on Github →

2024-04-04 10:53

Mathlib/Data/Int/Defs.lean

chore: Remove `Init.Data.Int.CompLemmas` (#11882) …

Added Int.natAbs_add_of_nonpos View on Github →