mathlib3
269bc85d - feat(analysis/matrix): add `frobenius_norm_conj_transpose` (#13883)

Commit

3 years ago

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

Author

eric-wieser

Parents