Commit 2025-01-30 06:18 1db0a08e

View on Github →

feat: lemmas about Matrix.comp for diagonal and stdBasis (#21181)

Estimated changes

Modified Mathlib/Data/Matrix/Composition.lean

added theorem Matrix.compAlgEquiv_apply

added theorem Matrix.compAlgEquiv_symm_apply

added theorem Matrix.comp_diagonal_diagonal

added theorem Matrix.comp_map_map

added theorem Matrix.comp_map_transpose

added theorem Matrix.comp_stdBasisMatrix_stdBasisMatrix

added theorem Matrix.comp_symm_diagonal

added theorem Matrix.comp_symm_stdBasisMatrix

added theorem Matrix.comp_symm_transpose

added theorem Matrix.comp_transpose