Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.frobenius_norm_diagonal

Modification history

2022-05-02 06:04

src/analysis/matrix.lean

feat(analysis/matrix): define the frobenius norm on matrices (#13497)

Added matrix.frobenius_norm_diagonal View on Github →