Theorem Matrix.liftLinear_single

Modification history

2025-08-14 03:21
Mathlib/Data/Matrix/Basis.lean
chore: fixes around `Matrix.liftLinear` (#28368) …
Added Matrix.liftLinear_singleView on Github →