Commit 2025-11-23 19:05 9e3e2a68
View on Github →refactor: clean up occurrences of Splits (p.map (RingHom.id _)) (#31915)
This cleans up some lingering debt from #31631 (as pointed out by @Vierkantor).
There's still plenty of mess in the Splits.lean file, but that will get taken care of in a followup PR where we switch over to the API in Factors.lean. So I've left theorem names mentioning splits_id as-is to avoid deprecated aliases at this point.