mathlib

811da369 - feat(representation_theory/group_cohomology_resolution): show k[G^(n + 1)] is free over k[G] (#15501)

feat(representation_theory/group_cohomology_resolution): show k[G^(n + 1)] is free over k[G] (#15501) Defines an isomorphism $k[G^{n + 1}] \cong k[G] \otimes_k k[G^n].$ Also shows that given a $k$-algebra $R$ and a $k$-basis for a module $M,$ we get an $R$-basis of $R \otimes_k M.$ Then, using that, we show $k[G^{n + 1}]$ is free.