Theorem Matrix.liftLinear_singleLinearMap

Modification history

2025-06-26 20:11
Mathlib/Data/Matrix/Basis.lean
feat: Add `Matrix.liftLinear` (#25845) …
Added Matrix.liftLinear_singleLinearMapView on Github →