[Merged by Bors] - refactor(representation_theory/group_cohomology_resolution): refactor k[G^{n + 1}] isomorphism

[101damnations]

This refactors the isomorphism $k[G^{n + 1}] \cong k[G] \otimes_k k[G^n]$ (where $G$ acts by left multiplication on $k[G^{n + 1}]$ and $k[G]$ but trivially on $k[G^n]$) to use an isomorphism of $G$-sets $G^{n + 1} \cong G \times G^n.$

---

This PR doesn't really need to exist but I got carried away.
I generalised the definition of representation.trivial, but can undo this if necessary.

[kbuzzard]

Thanks! This looks fine to me -- I've left some comments. I managed to golf two proofs (reducing two inductions to one) and this is probably worth including if you can't see any disadvantages with my potential definition change.

[semorrison]

@101damnations, could you resolve the conflicts? Feel free to ping me afterwards, I'd like to get this in!

[101damnations]

@semorrison Thank you, I've sorted the conflicts

[semorrison]

Is this meant to be labelled awaiting-review? If you don't label it, it won't appear on the #queue.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests