Theorem Matrix.IsHermitian.eigenvectorMatrix_mul_inv
Modification history
2024-05-04 18:40
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
refactor: new definition of `eigenvectorUnitary` (#11363) …
Deleted Matrix.IsHermitian.eigenvectorMatrix_mul_invView on Github →