Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-17 21:45 bbf5d1a5

View on Github →

refactor(algebra/field): partially migrate to bundled homs (#1999)

  • refactor(algebra/field): partially migrate to bundled homs
  • Add a few @[simp] attrs

Estimated changes

modified theorem is_ring_hom.injective
modified theorem is_ring_hom.map_div'
modified theorem is_ring_hom.map_div
modified theorem is_ring_hom.map_eq_zero
modified theorem is_ring_hom.map_inv'
modified theorem is_ring_hom.map_inv
modified theorem is_ring_hom.map_ne_zero
added theorem ring_hom.injective
added theorem ring_hom.map_div'
added theorem ring_hom.map_div
added theorem ring_hom.map_eq_zero
added theorem ring_hom.map_inv'
added theorem ring_hom.map_inv
added theorem ring_hom.map_ne_zero
added theorem ring_hom.map_fpow'
added theorem ring_hom.map_fpow