theorem HexRootsMathlib.rouche {f g : Polynomial ℂ} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : ∀ z ∈ Metric.sphere c R, ‖Polynomial.eval z f - Polynomial.eval z g‖ < ‖Polynomial.eval z g‖) : rootsInDisc f c R = rootsInDisc g c R

Classical Rouché theorem for complex polynomials on a circle, with roots counted with multiplicity in the enclosed open disc.

theorem HexRootsMathlib.rouche_symmetric {f g : Polynomial ℂ} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : ∀ z ∈ Metric.sphere c R, ‖Polynomial.eval z f - Polynomial.eval z g‖ < ‖Polynomial.eval z f‖ + ‖Polynomial.eval z g‖) : rootsInDisc f c R = rootsInDisc g c R

Symmetric Rouché theorem: strictness in the triangle inequality on the boundary circle is enough to give equal root counts in the disc.