refactor(FieldTheory): split Mathlib.FieldTheory.Purelyinseparable (#21343)
Mathlib.FieldTheory.Purelyinseparable