Commit 2021-03-27 06:35 cc7e722a
View on Github →refactor(representation_theory/maschke): replaces ¬(ring_char k ∣ fintype.card G) with invertible (fintype.card G : k) instance (#6901)
Refactors Maschke's theorem to take an instance of invertible (fintype.card G : k) instead of an explicit not_dvd : ¬(ring_char k ∣ fintype.card G).
Provides that instance in the context char_zero k.
Allows monoid_algebra.submodule.is_complemented to be an instance.