chore(ring_theory/localization/away): split (#19041)
This breaks off a large initial segment of the [longest chain](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/359494005) remaining to port.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
