Commit 2025-10-07 08:33 53db35fb

feat(RingTheory/Presentation): core of a presentation (#24794) If P is a presentation of S as an R-algebra and R₀ a subring of R containing the coefficients of the relations of P, then there exists an R₀-algebra S₀ such that S is isomorphic to the base change of S₀ to R. This is a tool to remove Noetherian hypothesis in certain situations.