Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-02 21:14 2568d41b

View on Github →

feat(data/matrix/basic): Add bundled versions of matrix.diagonal (#8510) Also shows injectivity of diagonal.

Estimated changes

Modified src/data/matrix/basic.lean

modified def matrix.diagonal

modified theorem matrix.diagonal_add

added def matrix.diagonal_add_monoid_hom

added def matrix.diagonal_alg_hom

added theorem matrix.diagonal_injective

added def matrix.diagonal_linear_map

added def matrix.diagonal_ring_hom

added theorem matrix.diagonal_smul