Commit 2025-08-14 11:29 41112046

View on Github →

feat: semilinearize LinearMap.mapMatrix and LinearEquiv.mapMatrix (#28358) I don't have a particularly strong motivation here, but the generalization is trivial, and I wanted to check if it conflicted with the work in #28359 (it does not, but that PR now depends on this one).

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

modified theorem LinearEquiv.entryLinearMap_comp_mapMatrix

modified def LinearEquiv.mapMatrix

modified theorem LinearEquiv.mapMatrix_symm

modified theorem LinearEquiv.mapMatrix_toLinearMap

modified theorem LinearEquiv.mapMatrix_trans

modified theorem LinearMap.entryLinearMap_comp_mapMatrix

modified def LinearMap.mapMatrix

modified theorem LinearMap.mapMatrix_comp

Modified Mathlib/Data/Matrix/Defs.lean