Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-05 06:07 de377ea3

View on Github →

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

Estimated changes

deleted theorem is_field_hom.injective
deleted theorem is_field_hom.map_div'
deleted theorem is_field_hom.map_div
deleted theorem is_field_hom.map_eq_zero
deleted theorem is_field_hom.map_inv'
deleted theorem is_field_hom.map_inv
deleted theorem is_field_hom.map_ne_zero
deleted def is_field_hom
added theorem is_ring_hom.injective
added theorem is_ring_hom.map_div'
added theorem is_ring_hom.map_div
added theorem is_ring_hom.map_inv'
added theorem is_ring_hom.map_inv
deleted theorem is_field_hom.map_fpow
added theorem is_ring_hom.map_fpow
modified theorem polynomial.degree_map
modified theorem polynomial.map_div
modified theorem polynomial.map_eq_zero
modified theorem polynomial.map_mod
modified theorem polynomial.nat_degree_map
modified theorem polynomial.splits_map_iff