Commit 2020-06-01 21:26 66ce5d07

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)].