Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 14:29 2f38ccb4

View on Github →

chore(data/matrix/basic): add lemmas about powers of matrices (#13815) Shows that:

natural powers commute with transpose, conj_transpose, diagonal, block_diagonal, and block_diagonal'.
integer powers commute with transpose, and conj_transpose.

Estimated changes

Modified src/data/matrix/basic.lean

modified theorem matrix.conj_transpose_list_prod

added theorem matrix.conj_transpose_pow

modified def matrix.conj_transpose_ring_equiv

added theorem matrix.diagonal_pow

added theorem matrix.map_injective

added theorem matrix.transpose_pow

Modified src/data/matrix/block.lean

added theorem matrix.block_diagonal'_pow

added theorem matrix.block_diagonal_pow

Modified src/linear_algebra/matrix/zpow.lean

added theorem matrix.conj_transpose_zpow

added theorem matrix.transpose_zpow