[Merged by Bors] - chore: split Algebra.CharP.Basic, reduce imports in RingTheory.Multiplicity

[semorrison]

This was adding unnecessary imports to Data.ZMod.Basic.

---

Despite adding several files, this reduces the total number of transitive imports reported via:

import Mathlib

open Lean Meta
#eval show MetaM Nat from do
  let mut t := 0
  for (_, s) in (← getEnv).importGraph.transitiveClosure do
    t := t + s.size
  return t

(only by about 600 out of 5.3m, but it's a start :-)

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported