Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 269bc85d

View on Github →

feat(analysis/matrix): add frobenius_norm_conj_transpose (#13883) This also moves the existing lemmas about the elementwise norm to the same file.

Estimated changes

Modified src/analysis/matrix.lean

added theorem matrix.frobenius_nnnorm_conj_transpose

added theorem matrix.frobenius_norm_conj_transpose

added theorem matrix.nnnorm_conj_transpose

added theorem matrix.norm_conj_transpose

Modified src/analysis/normed_space/star/matrix.lean

deleted theorem matrix.nnnorm_conj_transpose

deleted theorem matrix.norm_conj_transpose