Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-12 18:52 1c449b6c

View on Github →

chore(algebra/field*, field_theory/subfield): drop some x ≠ 0, use division_ring (#2136)

  • chore(algebra/field*, field_theory/subfield): drop some x ≠ 0, use division_ring We have 0⁻¹=0 in division_ring now, so no need to assume field in ring_hom.map_inv etc.
  • Fix lint

Estimated changes

deleted theorem is_ring_hom.map_div'
deleted theorem is_ring_hom.map_inv'
deleted theorem neg_inv'
deleted theorem ring_hom.map_div'
deleted theorem ring_hom.map_inv'
deleted theorem is_ring_hom.map_fpow'
modified theorem is_ring_hom.map_fpow
deleted theorem ring_hom.map_fpow'
modified theorem ring_hom.map_fpow