# Commit 2020-06-01 21:26 66ce5d07

View on Github →feat(representation_theory/maschke): Maschke's theorem (#2762) The final theorem is

```
lemma monoid_algebra.submodule.exists_is_compl
(not_dvd : ¬(ring_char k ∣ fintype.card G)) (p : submodule (monoid_algebra k G) V) :
∃ q : submodule (monoid_algebra k G) V, is_compl p q
```

for `[field k]`

.
The core computation, turning a `k`

-linear retraction of `k[G]`

-linear map into a `k[G]`

-linear retraction by averaging over `G`

, happens over an arbitrary `[comm_ring k]`

in which `[invertible (fintype.card G : k)]`

.