mathlib3

3d32bf9c - feat(ring_theory/multiplicity,data/polynomial): add some `iff`s (#17731)

feat(ring_theory/multiplicity,data/polynomial): add some `iff`s (#17731) * Replace `multiplicity_eq_zero_of_not_dvd` with an `iff` lemma `multiplicity_eq_zero`. * Add `padic_val_nat.eq_zero_iff`. * Merge `polynomial.mem_root_set` and `polynomial.mem_root_set_iff` into `polynomial.mem_root_set_iff_of_ne`. * Add new `polynomial.mem_root_set` that does not assume `p ≠ 0`. * Do a similar modification to `polynomial.mem_root_set'`. * Add `polynomial.root_multiplicity_eq_zero_iff`, `polynomial.mem_roots'`, and `polynomial.root_multiplicity_pos'`. * Generalize `polynomial.root_set_maps_to` to `polynomial.root_set_maps_to'`, add new particular case `polynomial.root_set_maps_to`. * Add `polynomial.root_set_maps_to`, use it to golf some proofs. * Do not assume `[no_zero_smul_divisors _ _]` in `polynomial.aeval_eq_zero_of_mem_root_set`.