reindexAlgEquiv

Stream: mathlib4

[Kevin Buzzard]

Right now docs#Matrix.reindexAlgEquiv is

def reindexAlgEquiv (e : m ≃ n) : Matrix m m R ≃ₐ[R] Matrix n n R :=

for R a CommSemiring. But in fact @Edison Xie pointed out that this can be generalised to

def reindexAlgEquiv (e : m ≃ n) : Matrix m m A ≃ₐ[R] Matrix n n A :=

with [Algebra R A] and A not necessarily commutative (and he needs this for his work on Brauer groups). My question is whether reindexAlgEquiv should be redefined, or whether this new isomorphism should be a new declaration.

[Matthew Ballard]

Where is reindexAlgEquiv currently used?

[Edison Xie]

Matthew Ballard said:

Where is reindexAlgEquiv currently used?

LinearAlgebra.Matrix.Basis and LinearAlgebra.Matrix.Transvection iirc

[Eric Wieser]

I think it's fine to generalize it; just make R an explicit argument