mathlib3

cc7e722a - refactor(representation_theory/maschke): replaces `¬(ring_char k ∣ fintype.card G)` with `invertible (fintype.card G : k)` instance (#6901)

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.