Commit 2023-12-03 22:58 5b49f9f4

View on Github →

feat(Data/Matrix): scalar if commutes with every stdBasisMatrix (#7810) M is a scalar matrix if it commutes with every non-diagonal stdBasisMatrix.

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

added theorem Matrix.StdBasisMatrix.col_eq_zero_of_commute_stdBasisMatrix

added theorem Matrix.StdBasisMatrix.diag_eq_of_commute_stdBasisMatrix

added theorem Matrix.StdBasisMatrix.mem_range_scalar_of_commute_stdBasisMatrix

added theorem Matrix.StdBasisMatrix.row_eq_zero_of_commute_stdBasisMatrix