Theorem Int.natCast_natAbs

Modification history

2025-08-01 23:04

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

feat(*): add `simp`/`gcongr` attrs and use them (#27718) …

Modified Int.natCast_natAbs View on Github →

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.natCast_natAbs View on Github →

2024-04-03 11:58

Mathlib/Data/Int/Order/Basic.lean

chore(Data/Int): Rename `coe_nat` to `natCast` (#11637) …

Added Int.natCast_natAbs View on Github →