Mathlib Changelog
v4
Changelog
About
Github
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