Commit 2022-12-08 04:04 3d32bf9c

feat(ring_theory/multiplicity,data/polynomial): add some iffs (#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.