Mathlib Changelog
v4
Changelog
About
Github
Def
Matrix.toMatrixInnerProductSpace
Modification history
2025-11-18 22:43
Mathlib/Analysis/Matrix/Order.lean
chore(LinearAlgebra/Matrix/PosDef): rename `Matrix.InnerProductSpace.ofMatrix` (#30928) …
Added
Matrix.toMatrixInnerProductSpace
View on Github →