Theorem ring_char.eq_zero

chore(algebra/char_p): ring_char.eq is better in the other direction, with instances, and explicit arguments (#11439)

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