Theorems · Theorem · complex analysis

Polynomial.isCoveringMapOn_eval

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (p : Polynomial 𝕜),
  IsCoveringMapOn (fun x => Polynomial.eval x p)
    ((fun x => Polynomial.eval x p) '' {k | Polynomial.eval k (Polynomial.derivative p) = 0})ᶜ

Defined in

Mathlib.Analysis.Complex.CoveringMap

Cited by

1 results in Mathlib

Foundations

Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldProperSpace