mathlib3

1c449b6c - 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` (#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 Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>