refactor: switch to `IsAdjoinRoot`

IsAdjoinRoot and IsAdjoinRootMonic were introduced by @Vierkantor in mathlib3#17690, and it could be used to unify various constructions in the library to remove duplication of similar APIs.

Three main constructions that could have an IsAdjoinRoot "instance" are (1) AdjoinRoot, (2) Algebra.adjoin (singleton), and (3) IntermediateField.adjoin (singleton).

Currently there are AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly identifying (2) and (1), IntermediateField.adjoinRootEquivAdjoin identifying (1) and (3), and PowerBasis.equivOfRoot, PowerBasis.equivOfMinpoly and AdjoinRoot.equiv' which are morally all special cases of IsAdjoinRoot.aequiv.
(There's also PowerBasis.equivAdjoinSimple, but it's strange since I don't see why it can't just be topEquiv.)

And there are Algebra.adjoin.liftSingleton, AdjoinRoot.lift(Hom), AdjoinRoot.Minpoly.toAdjoin, PowerBasis.lift which should all be special cases of IsAdjoinRoot.lift(Hom). There are AdjoinRoot.equiv, PowerBasis.liftEquiv, PowerBasis.liftEquiv', and IntermediateField.algHomAdjoinIntegralEquiv identifying AlgHoms out of an AdjoinRoot with the roots the polynomial in another algebra, which we should unify with an IsAdjoinRoot version.

There are AdjoinRoot.powerBasis, AdjoinRoot.powerBasis', Algebra.adjoin.powerBasis, Algebra.adjoin.powerBasis', and IntermediateField.adjoin.powerBasis, which should all be special cases of IsAdjoinRootMonic.powerBasis.

If I'm missing some declarations that could potentially be unified, please comment.

cc @acmepjz @tb65536

Start with Mathlib/RingTheory/IsAdjoinRoot and its IsAdjoinRoot.aequiv, liftHom, and IsAdjoinRootMonic.powerBasis declarations. Compare the listed AdjoinRoot, Algebra.adjoin, IntermediateField.adjoin, and PowerBasis APIs to identify declarations that can be unified; done means the relevant duplicate constructions use the shared IsAdjoinRoot interfaces without leaving the named special cases unresolved.