Def Matrix.InnerProductSpace.ofMatrix

Modification history

2025-11-18 22:43
Mathlib/Analysis/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix/PosDef): rename `Matrix.InnerProductSpace.ofMatrix` (#30928) …
Deleted Matrix.InnerProductSpace.ofMatrixView on Github →
2025-11-18 11:33
Mathlib/Analysis/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix): import less analysis (#31518) …
Modified Matrix.InnerProductSpace.ofMatrixView on Github →
2023-06-15 17:27
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat: port LinearAlgebra.Matrix.PosDef (#5060) …
Added Matrix.InnerProductSpace.ofMatrixView on Github →