Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-18 17:03 5260ab8e

View on Github →

feat(ring_theory/matrix): diagonal matrices Joint work with Johan Commelin

Estimated changes

added def matrix.diagonal
added theorem matrix.diagonal_add
added theorem matrix.diagonal_mul
added theorem matrix.diagonal_neg
added theorem matrix.diagonal_one
added theorem matrix.diagonal_val_eq
added theorem matrix.diagonal_val_ne
added theorem matrix.diagonal_zero
added theorem matrix.mul_diagonal
added theorem matrix.mul_eq_mul
modified theorem matrix.mul_val'
modified theorem matrix.mul_val
modified theorem matrix.one_val_eq
modified theorem matrix.one_val_ne'
modified theorem matrix.one_val_ne