Commit 2026-01-13 18:40 3e3dca24
View on Github →feat(Algebra/MonoidAlgebra): R[M][N] ≃+* R[N][M] (#33492)
Prove that R[M × N] ≃+* R[N][M] and deduce that R[M][N] ≃+* R[N][M]. Add supporting Finsupp lemmas.
The ugly proofs are transitional and will be reworked in and after #25273.