mathlib

d2463aa3 - feat(ring_theory/algebraic): is_algebraic_of_larger_base_of_injective (#9433)