Commit 2020-10-06 15:23 74161277
View on Github →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.