Commit 2024-02-13 15:17 71296caa

View on Github →

feat(LinearAlgebra/Matrix): scalar if commutes with every nontrivial transvection (#7815) M is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix). Also adds iff versions and corrects the names of the lemmas in #7810

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.scalar_commute_iff

Modified Mathlib/Data/Matrix/Basis.lean

deleted theorem Matrix.StdBasisMatrix.col_eq_zero_of_commute_stdBasisMatrix

deleted theorem Matrix.StdBasisMatrix.diag_eq_of_commute_stdBasisMatrix

deleted theorem Matrix.StdBasisMatrix.mem_range_scalar_of_commute_stdBasisMatrix

deleted theorem Matrix.StdBasisMatrix.row_eq_zero_of_commute_stdBasisMatrix

added theorem Matrix.col_eq_zero_of_commute_stdBasisMatrix

added theorem Matrix.diag_eq_of_commute_stdBasisMatrix

added theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix'

added theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix

added theorem Matrix.mem_range_scalar_of_commute_stdBasisMatrix

added theorem Matrix.row_eq_zero_of_commute_stdBasisMatrix

modified theorem Matrix.smul_stdBasisMatrix

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

added theorem Matrix.mem_range_scalar_iff_commute_transvectionStruct

added theorem Matrix.mem_range_scalar_of_commute_transvectionStruct