Commit 2026-03-03 15:46 18100d90

feat(RingTheory): generalise perfection to monoids (#31007)

1. We generalise PerfectRing to monoids (without changing the name).
2. We move Submonoid.perfection and Ring.Perfection to the already existing Perfection namespace, which solves the problem that Ring.Perfection and its lemmas Perfection.xxx are in different namespaces. Also, the monoid perfection and ring perfection have the same underlying set, so this unify the two approaches.
3. Perfection.lift is now generalised to monoids: liftMonoidHom : (M →* N) ≃ (M →* Perfection N p) where M is a perfect monoid.