mathlib3

276f0652 - advances on removing ne_field assumption