Theorem op_nnnorm_mul

Modification history

2023-08-22 02:46
Mathlib/Analysis/NormedSpace/Star/Unitization.lean
feat: The norm on `Unitization` is a C⋆-norm (#5393) …
Deleted op_nnnorm_mulView on Github →
2023-05-21 08:32
Mathlib/Analysis/NormedSpace/Star/Mul.lean
feat: port Analysis.NormedSpace.Star.Mul (#4147)
Added op_nnnorm_mulView on Github →