Commit 2024-01-06 05:23 c6529053
View on Github →fix(Analysis/NormedSpace/OperatorNorm): muddled norm and nnnorm (#9473)
This is a lemma about nnnorm
, but it seems one of the arguments was forgotten.
fix(Analysis/NormedSpace/OperatorNorm): muddled norm and nnnorm (#9473)
This is a lemma about nnnorm
, but it seems one of the arguments was forgotten.