mathlib3

214f197b - refactor(field_theory/*): Move and golf `alg_hom.fintype` (#16114)

refactor(field_theory/*): Move and golf `alg_hom.fintype` (#16114) This PR moves `alg_hom.fintype` to `minpoly.lean` so that it can be used later (e.g., in `normal.lean`).