Commit 2022-07-25 10:24 d244509f

feat(data/matrix/basic): Add alg_equiv and linear_equiv instances for transpose. (#15386) transpose has natural bundlings as an alg_equiv and a linear_equiv for which we already have the substantial lemmas. Similarly, conj_transpose can be bundled as a linear_equiv. This also alters the other bundled versions to take explicit variables as this saves the need for many type annotations, and makes the necessary edits to fix proofs.