Def Matrix.ofAddEquiv

Modification history

2024-11-14 16:12

Mathlib/Data/Matrix/Basic.lean

chore(Data/Matrix): split `Basic.lean` into `Defs.lean` and `Mul.lean` (#18972) …

Modified Matrix.ofAddEquiv View on Github →

2024-10-24 00:12

Mathlib/Data/Matrix/Basic.lean

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

Added Matrix.ofAddEquiv View on Github →