mathlib

4f7603c7 - chore(data/matrix/basic): add more lemmas about `conj_transpose` and `smul` (#13938)

chore(data/matrix/basic): add more lemmas about `conj_transpose` and `smul` (#13938) Unfortunately the `star_module` typeclass is of no help here; see [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Is.20star_module.20sensible.20for.20non-commutative.20rings.3F/near/257272767) for some discussion. In the meantime, this adds the lemmas for the most frequent special cases.