FiniteDimensional instance for matrix rings

Stream: Is there code for X?

[Edison Xie]

Do we have that if A is FiniteDimensional algebra over a field K, then for any n natural, Matrix (Fin n) (Fin n) A is FiniteDimensional over K as well?

[Eric Wieser]

@loogle Matrix, Module.Finite

[loogle]

:search: Module.Finite.matrix, LinearMap.charpoly.eq_1, and 4 more

[Edison Xie]

Eric Wieser said:

loogle Matrix, Module.Finite

Yeah I don't think Module.Finite.matrix is the one since it's only Matrix (FIn n) (Fin n) R over itself

[Eric Wieser]

As far as I can tell that should be a very easy fix, PR welcome!

[Eric Wieser]

(replacing (Pi.basis fun _ => Pi.basisFun R _) with (Pi.basis fun _ => Pi.basis fun _ => basisOnA))

[Eric Wieser]

Done in #18098

[Kim Morrison]

Not sure what the awaiting-CI emoji is. :-)

[Edison Xie]

Nice, thanks a lot!