Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-30 00:32 c04bc6e9

View on Github →

refactor(representation_theory/group_cohomology_resolution): refactor k[G^{n + 1}] isomorphism (#18271) 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.$

Estimated changes