Def Matrix.liftLinear

Modification history

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