Commit 2026-01-20 19:54 1efe6ae3

View on Github →

feat(Analysis): (complex) polynomials as branched coverings (#33726) originally proposed by @urkud in #33425

Estimated changes

Modified Mathlib/Algebra/Polynomial/Roots.lean

added theorem Polynomial.preimage_eval_singleton

Modified Mathlib/Analysis/Complex/CoveringMap.lean

added theorem Polynomial.isCoveringMapOn_eval

Modified Mathlib/Topology/Algebra/Polynomial.lean

added theorem Polynomial.isClosedMap_eval

added theorem Polynomial.isProperMap_eval

Modified Mathlib/Topology/Covering/Basic.lean

added theorem IsClosedMap.isCoveringMapOn_of_openPartialHomeomorph

added theorem IsClosedMap.isEvenlyCovered_of_openPartialHomeomorph

added theorem IsCoveringMapOn.mono

added theorem IsCoveringMapOn.of_openPartialHomeomorph

added theorem IsDiscrete.of_openPartialHomeomorph

added theorem IsEvenlyCovered.of_openPartialHomeomorph