Theorem nnnorm_algebraMap_nNReal

Modification history

2024-02-09 13:35
Mathlib/Analysis/NormedSpace/Basic.lean
chore: rename declarations containing `nNReal` to `nnreal` (#10372)
Deleted nnnorm_algebraMap_nNRealView on Github →
2023-04-12 19:26
Mathlib/Analysis/NormedSpace/Basic.lean
feat: port Analysis.NormedSpace.Basic (#3280)
Added nnnorm_algebraMap_nNRealView on Github →