Theorem Matrix.IsHermitian.eigenvectorUnitary_transpose_apply

Modification history

2025-01-27 17:00
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
refactor: unapply matrix lemmas (#21091) …
Added Matrix.IsHermitian.eigenvectorUnitary_transpose_applyView on Github →