Theorem Matrix.linfty_op_norm_mul

Modification history

2024-02-04 13:16

Mathlib/Analysis/Matrix.lean

chore: rename op_norm to opNorm (#10185)

Deleted Matrix.linfty_op_norm_mul View on Github →

2023-08-16 09:33

Mathlib/Analysis/Matrix.lean

refactor(Data/Matrix): Eliminate `⬝` notation in favor of `HMul` (#6487) …

Modified Matrix.linfty_op_norm_mul View on Github →

2023-06-22 00:17

Mathlib/Analysis/Matrix.lean

feat: port Analysis.Matrix (#4490)

Added Matrix.linfty_op_norm_mul View on Github →