Theorem Matrix.liftLinear_piSingle

Modification history

2025-08-14 03:21
Mathlib/Data/Matrix/Basis.lean
chore: fixes around `Matrix.liftLinear` (#28368) …
Deleted Matrix.liftLinear_piSingleView on Github →
2025-06-26 20:11
Mathlib/Data/Matrix/Basis.lean
feat: Add `Matrix.liftLinear` (#25845) …
Added Matrix.liftLinear_piSingleView on Github →