Commit 2026-01-27 22:28 3d088603

View on Github →

feat(Analysis, Topology): more examples of covering maps involving the complex plane (#33766)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

modified theorem Polynomial.eval_X_pow

Modified Mathlib/Analysis/Complex/CoveringMap.lean

modified theorem Polynomial.isCoveringMapOn_eval

added theorem isCoveringMapOn_npow

added theorem isCoveringMapOn_zpow

added theorem isCoveringMap_npow

added theorem isCoveringMap_zpow

added theorem isQuotientCoveringMap_npow

added theorem isQuotientCoveringMap_zpow

Modified Mathlib/Analysis/Complex/OpenMapping.lean

added theorem AnalyticOnNhd.is_constant_or_isOpenMap

added theorem Complex.isOpenQuotientMap_pow

added theorem Complex.isOpenQuotientMap_pow_compl_zero

added theorem Complex.isOpenQuotientMap_zpow_compl_zero

added theorem Polynomial.C_eq_or_isOpenQuotientMap_eval

added theorem Polynomial.isOpenQuotientMap_eval

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

modified theorem AddCircle.toCircle_add

added theorem AddCircle.toCircle_neg

added theorem AddCircle.toCircle_nsmul

added theorem AddCircle.toCircle_zsmul

added theorem Circle.isQuotientCoveringMap_npow

added theorem Circle.isQuotientCoveringMap_zpow

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.eval_surjective

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem ker_zpowGroupHom_eq_rootsOfUnity

added theorem rootsOfUnity_eq_ker

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

added def Homeomorph.inv₀

Modified Mathlib/Topology/Algebra/Polynomial.lean

added theorem isClosedMap_pow