CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 ring of holomorphic functions on a complex domain is an integral domain

Statement

The holomorphic functions on a complex domain form an integral domain under pointwise addition and multiplication.

More explicitly, for a complex domain $Ω$ , the set $H (Ω)$ of holomorphic functions $Ω \to C$ is a commutative subring of the function ring $C^{Ω}$ (The ring $R^{X}$ of all functions from a set $X$ into a ring, with pointwise operations, Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication), its constant zero and one functions are distinct, and $f g = 0$ implies $f = 0$ or $g = 0$ (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors).

Facts & Assumptions

Given: A complex domain $Ω$ (A complex domain is a nonempty connected open subset of $C$ ); the field $C$ ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ); and the facts from Linearity, product, reciprocal, and quotient rules for complex derivatives that constants, sums, differences, and products of holomorphic functions are holomorphic, and that a holomorphic function nonzero at a point remains nonzero on some neighbourhood of that point.

[L1]

If two holomorphic functions on a complex domain agree on a set with an accumulation point in the domain, then they agree everywhere on the domain (Identity theorem for holomorphic functions).

[L2]

In a function ring the operations are pointwise, and its distinguished zero and one are the corresponding constant functions (The ring $R^{X}$ of all functions from a set $X$ into a ring, with pointwise operations).

[L3]

An integral domain is a commutative ring with distinct zero and one and with 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 the holomorphic algebra laws in the given facts, $H (Ω)$ contains the constant functions and is closed under pointwise addition, subtraction, and multiplication; [L2] and the field laws therefore make it a commutative subring of $C^{Ω}$ .

L2given

1.2

Since $Ω$ is nonempty and $0 \neq 1$ in $C$ , the constant zero and one functions take different values at any point of $Ω$ and are distinct.

givenalgebra

1.3

Suppose $f g$ is the zero function and $f$ is not the zero function. Choose $a \in Ω$ with $f (a) \neq 0$ . The given holomorphic algebra fact makes $f$ nonzero on a neighbourhood of $a$ , so $g$ vanishes there; [L1] then makes $g$ the zero function on $Ω$ . Thus a zero product has a zero factor.

L1givenchoose

2.1

Steps 1.1, 1.2, and 1.3 verify all clauses of [L3], so $H (Ω)$ is an integral domain.

step 1.1step 1.2step 1.3L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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, Guide to Cultivating Complex Analysis, Exercise 2.4.13(a) (standard reference, not scraped)