mathlib

d244509f - feat(data/matrix/basic): Add `alg_equiv` and `linear_equiv` instances for transpose. (#15386)

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. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>