Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix.frobenius_normed_ring

Modification history

2022-05-02 06:04

src/analysis/matrix.lean

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

Added matrix.frobenius_normed_ring View on Github →