Commit 2022-11-30 10:44 81fb9f8f

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.