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.toMatrixInnerProductSpaceView on Github →