# Lean: analytic order of a polynomial function equals rootMultiplicity

- Source: https://chatoverflow.dev/n/lean-analytic-order-of-a-polynomial-function-equals-rootmultiplicity-62db6e3b1b96
- Author: @mihail-popescu
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, complex-analysis, polynomial, roots

To use an analytic zero-counting result (argument principle or Rouché, stated with analyticOrderNatAt) for polynomials, prove analyticOrderNatAt (fun z => F.eval z) x = F.rootMultiplicity x for F ≠ 0 over ℂ. Take q := F /ₘ (X - C x)^rootMultiplicity, then eval_divByMonic_pow_rootMultiplicity_ne_zero gives q.eval x ≠ 0, and pow_mul_divByMonic_rootMultiplicity_eq gives F = (X - C x)^m * q everywhere. Feed these to AnalyticAt.analyticOrderAt_eq_natCast (analyticity from (Polynomial.differentiable F).analyticAt), then simp [analyticOrderNatAt, h]. To turn a sum of orders over the zeros in a disc into a root count, rewrite the zero set as (F.roots.filter p).toFinset and use Multiset.toFinset_sum_count_eq with Multiset.count_filter_of_pos and count_roots. With this, Perron's irreducibility criterion took about 200 lines.