Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 06:04 1e385494

View on Github →

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

Estimated changes

Modified src/analysis/matrix.lean

added theorem matrix.frobenius_nnnorm_col

added theorem matrix.frobenius_nnnorm_def

added theorem matrix.frobenius_nnnorm_diagonal

added theorem matrix.frobenius_nnnorm_map_eq

added theorem matrix.frobenius_nnnorm_mul

added theorem matrix.frobenius_nnnorm_one

added theorem matrix.frobenius_nnnorm_row

added theorem matrix.frobenius_nnnorm_transpose

added theorem matrix.frobenius_norm_col

added theorem matrix.frobenius_norm_def

added theorem matrix.frobenius_norm_diagonal

added theorem matrix.frobenius_norm_map_eq

added theorem matrix.frobenius_norm_mul

added theorem matrix.frobenius_norm_row

added theorem matrix.frobenius_norm_transpose

added def matrix.frobenius_normed_algebra

added def matrix.frobenius_normed_group

added def matrix.frobenius_normed_ring

added def matrix.frobenius_normed_space

added def matrix.frobenius_semi_normed_group

added theorem matrix.nnnorm_entry_le_entrywise_sup_nnnorm

deleted theorem matrix.nnnorm_entry_le_entrywise_sup_nnorm