Theorem Real.norm_natCast

Modification history

2024-08-29 12:34

Mathlib/Analysis/Normed/Group/Basic.lean

feat(RCLike): `nnnorm` lemmas (#16144) …

Modified Real.norm_natCast View on Github →

2024-04-07 17:47

Mathlib/Analysis/Normed/Group/Basic.lean

chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …

Added Real.norm_natCast View on Github →