Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.smul_eq_mul_diagonal

Modification history

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_mul_diagonalView on Github →