Commit 2022-05-05 07:41 4f7603c7
View on Github →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 for some discussion.
In the meantime, this adds the lemmas for the most frequent special cases.