Theorem Matrix.l2_opNNNorm_conjTranspose

Modification history

2024-03-21 09:38
Mathlib/Analysis/NormedSpace/Star/Matrix.lean
chore(Star/Matrix): drop `DecidableEq` assumptions (#11557)
Modified Matrix.l2_opNNNorm_conjTransposeView on Github →
2024-02-04 13:16
Mathlib/Analysis/NormedSpace/Star/Matrix.lean
chore: rename op_norm to opNorm (#10185)
Added Matrix.l2_opNNNorm_conjTransposeView on Github →