Theorem LinearMap.entryLinearMap_comp_mapMatrix

Modification history

2025-08-14 11:29

Mathlib/Data/Matrix/Basic.lean

feat: semilinearize `LinearMap.mapMatrix` and `LinearEquiv.mapMatrix` (#28358) …

Modified LinearMap.entryLinearMap_comp_mapMatrix View on Github →

2024-10-24 00:12

Mathlib/Data/Matrix/Basic.lean

feat(Matrix): extracting entries as a linear map (#17535) …

Added LinearMap.entryLinearMap_comp_mapMatrix View on Github →