mathlib

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

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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/multiplicity.20of.20root.20in.20extension.20field/near/286736361)