Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.linfty_op_norm_def

Modification history

2022-05-02 15:58
src/analysis/matrix.lean
feat(analysis/matrix): provide a normed_algebra structure on matrices (#13518) …
Added matrix.linfty_op_norm_defView on Github →