Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.linfty_op_nnnorm_mul_vec

Modification history

2022-11-17 13:13
src/analysis/matrix.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified matrix.linfty_op_nnnorm_mul_vecView on Github →
2022-05-02 15:58
src/analysis/matrix.lean
feat(analysis/matrix): provide a normed_algebra structure on matrices (#13518) …
Added matrix.linfty_op_nnnorm_mul_vecView on Github →