Commit 2022-06-21 00:01 87f47580

feat(polynomial/ring_division): strengthen/generalize various lemmas (#14839)

• Generalize the assumption function.injective f in le_root_multiplicity_map to map f p ≠ 0. Strictly speaking this is not a generalization because the trivial case p = 0 is excluded. If one do want to apply the lemma without assuming p ≠ 0, they can use the newly introduced eq_root_multiplicity_map, which is a strengthening of the original lemma (with the same hypothesis function.injective f).
• Extract some common variables from four lemmas.
• Generalize eq_of_monic_of_dvd_of_nat_degree_le to eq_leading_coeff_mul_of_monic_of_dvd_of_nat_degree_le: if a polynomial q is divisible by a monic polynomial p and has degree no greater than p, then q = p. Also remove the is_domain hypothesis and golf the proof. Zulip