Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix

Modification history

2021-08-26 13:06

src/data/matrix/basic.lean

feat(*): remove the `fintype` requirement from matrices. (#8810) …

Modified matrix View on Github →

2020-08-20 21:33

src/data/matrix/basic.lean

chore(data/matrix, linear_algebra): generalize universe parameters (#3879) …

Modified matrix View on Github →

2018-09-18 13:08

ring_theory/matrix.lean

feat(ring_theory/matrix): (finally!) adding matrices (#334) …

Added matrix View on Github →