Theorem Int.nnnorm_coe_nat

Modification history

2024-04-07 17:47
Mathlib/Analysis/NormedSpace/Int.lean
chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …
Deleted Int.nnnorm_coe_natView on Github →
2023-03-13 15:40
Mathlib/Analysis/NormedSpace/Int.lean
feat: port Analysis.NormedSpace.Int (#2848)
Added Int.nnnorm_coe_natView on Github →