mathlib

74161277 - feat(data/polynomial/ring_division): add multiplicity of sum of polynomials is at least minimum of multiplicities (#4442)

feat(data/polynomial/ring_division): add multiplicity of sum of polynomials is at least minimum of multiplicities (#4442) I've added the lemma `root_multiplicity_add` inside `data/polynomial/ring_division` that says that the multiplicity of a root in a sum of two polynomials is at least the minimum of the multiplicities. Co-authored-by: riccardobrasca <32490532+riccardobrasca@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Johan Commelin <johan@commelin.net>