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.




leanprover-community/mathlib,leanprover-community/mathlib