mathlib3

1e43208e - refactor(ring_theory): use `x ∈ non_zero_divisors` over `x : non_zero_divisors` (#7961)

refactor(ring_theory): use `x ∈ non_zero_divisors` over `x : non_zero_divisors` (#7961) `map_ne_zero_of_mem_non_zero_divisors` and `map_mem_non_zero_divisors` used to take `x : non_zero_divisors A` as an (implicit) argument. This is awkward if you only have `hx : x ∈ non_zero_divisors A`, requiring you to write out `@map_ne_zero_of_mem_non_zero_divisors _ _ _ _ _ _ hf ⟨x, hx⟩`. By making `x ∈ non_zero_divisors A` the explicit argument, we can avoid this annoyance. See e.g. `ring_theory/polynomial/scale_roots.lean` for the improvement.