mathlib3

6f38a50d - feat(field_theory/minimal_polynomial): add algebra_map_inj (#5062)

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.