Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.frobenius_norm_mul

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.frobenius_norm_mulView on Github →
2022-05-02 06:04
src/analysis/matrix.lean
feat(analysis/matrix): define the frobenius norm on matrices (#13497)
Added matrix.frobenius_norm_mulView on Github →