Theorem LinearEquiv.mapMatrix_toLinearMap

Modification history

2025-08-14 11:29

Mathlib/Data/Matrix/Basic.lean

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

Modified LinearEquiv.mapMatrix_toLinearMap View on Github →

2024-10-24 00:12

Mathlib/Data/Matrix/Basic.lean

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

Added LinearEquiv.mapMatrix_toLinearMap View on Github →