Commit 2025-10-12 13:56 ef123dc3

refactor(RingTheory/FinitePresentation): generalise instances (#30455) Previously, they only proved that R[X] (or alike) is finitely presented over R. Now they prove that A[X] is finite presented over R if A is. As a result, generalise the (non-)instance for AdjoinRoot and make it an instance