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.

Estimated changes