mathlib

260d6533 - feat(algebra/field): remove is_field_hom

feat(algebra/field): remove is_field_hom A field homomorphism is just a ring homomorphism. This is one trivial tiny step in moving over to bundled homs.