Commit 2020-12-03 19:30 6f38a50d

feat(field_theory/minimal_polynomial): add algebra_map_inj (#5062) I have added algebra_map_inj that computes the minimal polynomial of an element of the base ring. It generalizes algebra_map that assumes the base ring to be a field. I left algebra_map since I think it is reasonable to have a lemma that works without proving explicitly that the algebra map is injective.