Commit 2022-07-15 01:25 8d749e60

refactor(field_theory/*): Replace weaker alg_hom.fintype with stronger alg_hom.fintype (#15345) Mathlib has two instances of alg_hom.fintype. The version in field_theory.fixed is weaker (it assumes finite-dimensionality of the target). The version in field_theory.primitive_element is stronger (it does not assume finite-dimensionality of the target). So why not replace the weaker version by the stronger version?