Theorem Matrix.l2_op_nnnorm_conjTranspose_mul_self

Modification history

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

chore: rename op_norm to opNorm (#10185)

Deleted Matrix.l2_op_nnnorm_conjTranspose_mul_self View on Github →

2024-01-09 23:05

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

chore(Analysis.NormedSpace.Star.Matrix): add missing `nnnorm` lemmas (#9600)

Added Matrix.l2_op_nnnorm_conjTranspose_mul_self View on Github →