Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.smul_eq_diagonal_mul

Modification history

2021-08-26 13:06

src/data/matrix/basic.lean

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

Modified matrix.smul_eq_diagonal_mul View on Github →

2020-02-08 10:42

src/data/matrix/basic.lean

feat(linear_algebra): The Special linear group SL(n, R) (#1960) …

Added matrix.smul_eq_diagonal_mul View on Github →