Theorem Matrix.linfty_op_nnnorm_toMatrix

Modification history

2024-02-04 13:16

Mathlib/Analysis/Matrix.lean

chore: rename op_norm to opNorm (#10185)

Deleted Matrix.linfty_op_nnnorm_toMatrix View on Github →

2024-01-06 09:51

Mathlib/Analysis/Matrix.lean

feat(Analysis/Matrix): `linfty_op_nnnorm` agrees with the operator norm (#9476) …

Added Matrix.linfty_op_nnnorm_toMatrix View on Github →