Commit 2020-11-10 23:30 5c9e3ef8

View on Github →

feat(ring_theory/adjoin_root): Dimension of adjoin_root (#4830) Adds adjoin_root.degree_lt_linear_equiv, the restriction of 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.

Estimated changes