Commit 2022-05-05 14:55 ec44f459

View on Github →

feat(data/matrix/basic): even more lemmas about conj_transpose and smul (#13970) It turns out none of the lemmas in the previous #13938 were the ones I needed.

Estimated changes

Modified src/algebra/star/module.lean

added theorem star_int_cast_smul

added theorem star_inv_int_cast_smul

added theorem star_inv_nat_cast_smul

added theorem star_nat_cast_smul

added theorem star_rat_cast_smul

Modified src/data/matrix/basic.lean

added theorem matrix.conj_transpose_int_cast_smul

added theorem matrix.conj_transpose_inv_int_cast_smul

added theorem matrix.conj_transpose_inv_nat_cast_smul

added theorem matrix.conj_transpose_nat_cast_smul

added theorem matrix.conj_transpose_rat_cast_smul