mathlib3

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

#2136

Merged