Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.is_hermitian_diagonal_of_self_adjoint

Modification history

2023-03-19 20:21

src/linear_algebra/matrix/hermitian.lean

refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565) …

Added matrix.is_hermitian_diagonal_of_self_adjoint View on Github →