mathlib

017e1f13 - feat(ring_theory/algebraic): `is_algebraic_algebra_map_iff` (#15586)

feat(ring_theory/algebraic): `is_algebraic_algebra_map_iff` (#15586) This PR adds `is_algebraic_algebra_map_iff`, which is the `is_algebraic` analog of `is_integral_algebra_map_iff`. I also added the special case of an `intermediate_field`, which has been useful.