mathlib

a4b6c418 - feat(field_theory/separable): is_separable_of_alg_hom_is_separable (#5175)

feat(field_theory/separable): is_separable_of_alg_hom_is_separable (#5175) Proves that is_separable pulls back along an alg_hom Co-authored-by: tb65536 <tb65536@users.noreply.github.com>