Commit 2025-11-18 11:33 1c10cebd

View on Github →

chore(LinearAlgebra/Matrix): import less analysis (#31518) Follow up to #31480. Also fix a few namespacing issues that arose.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Created Mathlib/Analysis/Matrix/Hermitian.lean

added theorem Matrix.IsHermitian.coe_re_apply_self

added theorem Matrix.IsHermitian.coe_re_diag

added theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self

added theorem Matrix.isHermitian_iff_isSymmetric

Renamed Mathlib/LinearAlgebra/Matrix/LDL.lean to Mathlib/Analysis/Matrix/LDL.lean

Modified Mathlib/Analysis/Matrix/PosDef.lean

added def Matrix.InnerProductSpace.ofMatrix

modified theorem Matrix.IsHermitian.posDef_iff_eigenvalues_pos

modified theorem Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg

modified theorem Matrix.PosDef.det_pos

modified theorem Matrix.PosDef.eigenvalues_pos

added theorem Matrix.PosDef.re_dotProduct_pos

modified theorem Matrix.PosSemidef.det_nonneg

modified theorem Matrix.PosSemidef.eigenvalues_nonneg

added theorem Matrix.PosSemidef.re_dotProduct_nonneg

modified theorem Matrix.PosSemidef.trace_eq_zero_iff

Modified Mathlib/Analysis/Matrix/Spectrum.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

deleted theorem Matrix.IsHermitian.coe_re_apply_self

deleted theorem Matrix.IsHermitian.coe_re_diag

deleted theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self

deleted theorem Matrix.isHermitian_iff_isSymmetric

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

deleted def Matrix.InnerProductSpace.ofMatrix

deleted theorem Matrix.PosDef.re_dotProduct_pos

deleted theorem Matrix.PosSemidef.re_dotProduct_nonneg