mathlib3
de377ea3 - feat(algebra/field): remove is_field_hom (#1777)

Commit
6 years ago
feat(algebra/field): remove is_field_hom (#1777) * 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. * Fix up nolints.txt * Remove duplicate instances
Author
Committer
Parents
Loading