Commit 2024-10-24 00:12 ed804870

View on Github →

feat(Matrix): extracting entries as a linear map (#17535) Strictly speaking, something like this was available as LinearMap.proj, but actually using it in practice is awkward as unification struggles (see line 1227 in this PR). I'm happy to take name suggestions, as well as ideas for other generalities.

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem AddEquiv.entryAddHom_comp_mapMatrix

added theorem AddMonoidHom.entryAddMonoidHom_comp_mapMatrix

added theorem LinearEquiv.entryLinearMap_comp_mapMatrix

added theorem LinearEquiv.mapMatrix_toLinearMap

added theorem LinearMap.entryLinearMap_comp_mapMatrix

added theorem Matrix.coe_ofAddEquiv

added theorem Matrix.coe_ofAddEquiv_symm

added theorem Matrix.coe_ofLinearEquiv

added theorem Matrix.coe_ofLinearEquiv_symm

added def Matrix.entryAddHom

added theorem Matrix.entryAddHom_eq_comp

added def Matrix.entryAddMonoidHom

added theorem Matrix.entryAddMonoidHom_eq_comp

added theorem Matrix.entryAddMonoidHom_toAddHom

added def Matrix.entryLinearMap

added theorem Matrix.entryLinearMap_eq_comp

added theorem Matrix.entryLinearMap_toAddHom

added theorem Matrix.entryLinearMap_toAddMonoidHom

added theorem Matrix.evalAddMonoidHom_comp_diagAddMonoidHom

added def Matrix.ofAddEquiv

added def Matrix.ofLinearEquiv

added theorem Matrix.proj_comp_diagLinearMap