Theorem NNReal.natCast_natAbs

Modification history

2024-06-23 06:39

Mathlib/Analysis/Normed/Group/Basic.lean

chore: split some results out of Analysis.Normed.Group.Basic (#14035) …

Modified NNReal.natCast_natAbs View on Github →

2024-04-03 11:58

Mathlib/Analysis/Normed/Group/Basic.lean

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

Added NNReal.natCast_natAbs View on Github →