Commit 2025-01-27 17:00 0a8db061

View on Github →

refactor: unapply matrix lemmas (#21091) These are slightly more convenient expressed in terms of vector operations. ext; simp can always be used to restore them to the applied versions.

Estimated changes

Modified Mathlib/Data/Matrix/Mul.lean

modified theorem Matrix.mulVec_one

added theorem Matrix.one_vecMul

deleted theorem Matrix.vec_one_mul

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

added theorem Matrix.IsHermitian.eigenvectorUnitary_transpose_apply

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean