Ideals in a matrix ring

Stream: Is there code for X?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am looking for the result that the Jacobson radical of a matrix ring over $R$ is the ideal of matrices with entries in the Jacobson radical of $R$ ($J(M_n(R)) = M_n(J(R))$), but I couldn't find the result or even a definition of the latter entity (matrices with entries in an ideal of the base ring). Is there anything along these lines in mathlib? If not, would a PR adding this be welcome?

[Johan Commelin]

PR certainly welcome!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I see there are some results about $M_n(I)$ in FLT.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I started this in #17750, and concluded in #17756.