feat(ring_theory/adjoin_root): Dimension of adjoin_root (#4830)
Adds `adjoin_root.degree_lt_linear_equiv`, the restriction of `adjoin_root.mk f`
to the polynomials of degree less than `f`, viewed as a isomorphism between
vector spaces over `K` and uses it to prove that `adjoin_root f` has dimension
`f.nat_degree`. Also renames `adjoin_root.alg_hom` to `adjoin_root.lift_hom`.
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
