mathlib3
8d749e60 - refactor(field_theory/*): Replace weaker `alg_hom.fintype` with stronger `alg_hom.fintype` (#15345)

Commit
3 years ago
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? Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Author
Parents
Loading