feat(ring_theory): `is_adjoin_root` predicate (#17690)
This PR introduces the `is_adjoin_root S f` structure which states the ring/field `S` is generated by adjoining a specified root of the polynomial `f : R[X]` to `R`. This is essentially the predicate counterpart of `adjoin_root`, in the vein of `is_integral_closure` and `is_localization`. Like `power_basis`, there are multiple possible roots we can choose for a given `S` and `f`, so it's a structure rather than a typeclass. Using a predicate on a ring, rather than constructing the ring explicitly, allows us to view the same ring in different bases. For example, we want to treat `ℚ((1-√-3)/2)` the same as `ℚ(√-3)` while keeping `ℤ[(1-√-3)/2]` and `ℤ[√-3]` distinct.
`power_basis` is less suitable for this purpose: `is_adjoin_root` explicitly allows us to specify which polynomial we want to adjoin the root of, in contrast to `power_basis` which does provide a minimal polynomial but this might not be the one we started out with.
We also define an `is_adjoin_root_monic S f` structure, which extends `is_adjoin_root` by additionally specifying that `f` is monic. This provides a few usability advantages when `f` is specified explicitly such as `is_adjoin_root_monic ℚ(√-3) (X^2 + C 3)`, since we don't have to carry around the `monic f` hypothesis everywhere. In particular, if `f` is monic we can represent elements of `S` uniquely as low-degree polynomials and construct a power basis, so this really provides more expressive power.
The contents of this PR are based on our project on formalized computations of the class number and solutions of Mordell equations.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
