CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The holomorphic functions on a domain in $C^{m}$ have no zero divisors

Statement

Let $m \geq 1$ and let $U \subseteq C^{m}$ be a nonempty connected open set. Under pointwise addition and multiplication, the holomorphic functions $U \to C$ form an integral domain: if $f, g : U \to C$ are holomorphic and $f g \equiv 0$ , then $f \equiv 0$ or $g \equiv 0$ .

Facts & Assumptions

Given: A nonempty connected open set $U \subseteq C^{m}$ and holomorphic functions $f, g : U \to C$ .

[L1]

A holomorphic function vanishing on a nonempty open subset of a connected open set in $C^{m}$ vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L2]

Sums, products and nonvanishing quotients of holomorphic functions are holomorphic (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).

[L3]

A holomorphic function of several variables is continuous (A holomorphic function of several variables is continuous and separately holomorphic).

[L4]

An integral domain is a commutative ring with $1 \neq 0$ and no zero divisors (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors).

Proof

technique · direct

1.1

By [L2], the holomorphic functions on $U$ are closed under pointwise addition and multiplication, and pointwise operations are commutative and associative because they are so in $C$ ; the constant functions $0$ and $1$ are holomorphic, and $1 \neq 0$ , so this is a nonzero commutative ring.

givenL2

1.2

Suppose $f g \equiv 0$ and $f \equiv̸ 0$ . Since $f$ is continuous by [L3], the set $V : = {z \in U : f (z) \neq 0}$ is open in $U$ ; it is nonempty because $f$ is not identically zero; and for every $z \in V$ the equality $f (z) g (z) = 0$ in $C$ forces $g (z) = 0$ , so $g$ vanishes on the nonempty open set $V$ .

givenL3

2.1

Apply [L1] to $g$ and the open set $V$ : then $g \equiv 0$ on $U$ . So $f g \equiv 0$ implies $f \equiv 0$ or $g \equiv 0$ , and with step 1.1 this is exactly the zero-divisor clause of [L4]; therefore the ring of holomorphic functions on $U$ is an integral domain.

step 1.1step 1.2L1L4∎

Remarks

Connectedness matters. On a disconnected open set, a function may vanish on one component and not on another, so the product of two nonzero holomorphic functions can be zero. The corollary is therefore genuinely about domains, not arbitrary open sets.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

J. Lebl, Tasty Bits of Several Complex Variables, v4.4, Def. 1.2.9 and Ex. 1.2.19 (standard reference, not scraped)

The holomorphic functions on a domain in CmCm have no zero divisors