Def Matrix.entryLinearMap

Modification history

2026-09-18 14:05

Mathlib/Data/Matrix/Basic.lean

doc(Matrix): mention bundled forms in docstrings (#41438) …

Modified Matrix.entryLinearMap View on Github →

2024-10-24 00:12

Mathlib/Data/Matrix/Basic.lean

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

Added Matrix.entryLinearMap View on Github →