Commit 2025-06-26 20:11 e3af7257

View on Github →

feat: Add Matrix.liftLinear (#25845) This behaves similarly to LinearMap.lsum, and slightly golfs an existing definition.

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

added def Matrix.liftLinear

added theorem Matrix.liftLinear_comp_singleLinearMap

added theorem Matrix.liftLinear_piSingle

added theorem Matrix.liftLinear_singleLinearMap

Modified Mathlib/LinearAlgebra/Pi.lean

modified theorem LinearMap.lsum_single

Modified Mathlib/RingTheory/MatrixAlgebra.lean