Commit 2026-03-05 10:25 a2403213

feat(RingTheory): isomorphism between perfection of R and perfection of R/I (#36161) We construct the following isomorphism:

def Perfection.quotientMulEquiv (p : ℕ) [Fact (Nat.Prime p)]
    {R : Type*} [CommRing R] (I : Ideal R) [CharP (R ⧸ I) p] [IsAdicComplete I R] :
    Perfection R p ≃* Perfection (R ⧸ I) p

I also removed simp lemmas which expose the raw definition and instead prioritised lemmas which talk about the intended constructors, i.e. for x : Perfection R p we don't want x.1 n and instead want x.coeff R p n, and when M is perfect then maps M -> Perfection N p is determined by the zeroth coefficients.