Theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self

Modification history

2025-11-18 11:33
Mathlib/Analysis/Matrix/Hermitian.lean
chore(LinearAlgebra/Matrix): import less analysis (#31518) …
Modified Matrix.IsHermitian.im_star_dotProduct_mulVec_selfView on Github →
2025-09-09 13:02
Mathlib/LinearAlgebra/Matrix/Hermitian.lean
feat(Analysis/InnerProductSpace/Positive): `A.toEuclideanLin.IsPositive` iff `A.PosSemidef` (#28553)
Added Matrix.IsHermitian.im_star_dotProduct_mulVec_selfView on Github →