Theorem Matrix.l2_opNorm_conjTranspose

Modification history

2024-03-21 09:38

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

chore(Star/Matrix): drop `DecidableEq` assumptions (#11557)

Modified Matrix.l2_opNorm_conjTranspose View on Github →

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

chore: rename op_norm to opNorm (#10185)

Added Matrix.l2_opNorm_conjTranspose View on Github →