Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order

Statement

Let Ω be a homologically simply connected complex domain, let f:Ω→C be holomorphic and nowhere zero, and let m be a natural number with m≥1. Then there is a holomorphic, nowhere-zero q:Ω→C with

q(z)m=f(z)(z∈Ω).

One such q is exp⁡(L/m) for any holomorphic logarithm L of f; replacing L by another holomorphic logarithm of f multiplies q by an mth root of unity.

Facts & Assumptions

Given: A homologically simply connected complex domain Ω, a holomorphic nowhere-zero f:Ω→C, and a natural m≥1.

[L1]

On a homologically simply connected complex domain, a holomorphic nowhere-zero f admits a holomorphic L with exp⁡∘L=f, and any two such differ by a constant in 2πiZ (A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm, Homologically simply connected complex domains).

[L2]

exp⁡(z+w)=exp⁡zexp⁡w for all complex z,w (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

[L3]

The complex exponential is entire with exp⁡′=exp⁡ (The complex exponential is entire and its complex derivative is itself).

[L4]

The composite of functions complex differentiable at the relevant points is complex differentiable, with (g∘f)′(a)=g′(f(a))f′(a) (The chain rule for complex derivatives); constant multiples of complex differentiable functions are complex differentiable (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L5]

For a natural m≥1, the mth roots of unity are exactly the numbers exp⁡(2πik/m) for natural k with 0≤k<m (The n-th roots of a complex number and the n distinct roots of unity for every n≥1).

[L6]

Natural powers satisfy z0=1 and zj+1=zjz (Integer powers in the complex field).

[L7]

If a property holds at 0 and passes from j to j+1, it holds for every natural number (The principle of mathematical induction).

Proof

technique · direct
1.1givenL1L3L4

By [L1] fix a holomorphic L on Ω with exp⁡∘L=f, and put q=exp⁡(L/m), which is holomorphic on Ω by [L3] and [L4].

1.2L8

The exponential never vanishes, since ∣exp⁡v∣=eRe⁡v>0 by [L8]; so q is nowhere zero.

2.1step 1.1L2L6L7

An induction on j ([L7]) using [L2] and [L6] gives exp⁡(v)j=exp⁡(jv) for every complex v and every natural j, the case j=0 reading 1=exp⁡(0). Taking j=m and v=L(z)/m gives q(z)m=exp⁡(L(z))=f(z).

3.1step 1.1step 2.1L1L2L5L9∎

If L1 is another holomorphic logarithm of f then L1=L+2πik for a fixed integer k by [L1] and [L9], so exp⁡(L1/m)=exp⁡(L/m)exp⁡(2πik/m) by [L2], and exp⁡(2πik/m) is an mth root of unity by [L5].

Depends on

Used by

Dependency tree · two levels

61 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources