mathlib
a4e0a656 - feat(linear_algebra/matrix/hermitian): complex_hermitian_real_diagonal (#16380)

Commit
3 years ago
feat(linear_algebra/matrix/hermitian): complex_hermitian_real_diagonal (#16380) The diagonal elements of a complex Hermitian matrix are real.
Author
Parents
Loading