basic): even more lemmas about `conj_transpose` and `smul` (#13970)

Commit

3 years ago

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.

Author

eric-wieser

Parents

420fabf7

mathlib3 ec44f459 - feat(data/matrix/basic): even more lemmas about `conj_transpose` and `smul` (#13970)

mathlib3
ec44f459 - feat(data/matrix/basic): even more lemmas about `conj_transpose` and `smul` (#13970)