Def Matrix.toInnerProductSpace

Modification history

2025-11-18 22:43
Mathlib/Analysis/Matrix/PosDef.lean
chore(LinearAlgebra/Matrix/PosDef): rename `Matrix.InnerProductSpace.ofMatrix` (#30928) …
Added Matrix.toInnerProductSpaceView on Github →