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.
Real and imaginary parts, complex conjugation, and modulus
Definition
Every has unique coordinates ( is a field, every element is uniquely , and every nonzero element has inverse ). Define and define its modulus by The real numbers are least-upper-bound complete (The Cauchy-sequence reals have the least-upper-bound property), so the nonnegative square root exists and is unique by Square roots exist: a unique with ; the positives are .
Depends on
- $\mathbb C=\mathbb R[x]/(x^2+1)$ is a field, every element is uniquely $a+bi$, and every nonzero element has inverse $(a-bi)/(a^2+b^2)$
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- The Cauchy-sequence reals have the least-upper-bound property
Used by
- A holomorphic function with continuous complex derivative has C¹ real and imaginary components Corollary
- The induced length is a norm Corollary
- The inner-product norm is definite, homogeneous, and satisfies the triangle inequality Corollary
- The principal logarithm is the normalised holomorphic branch on the slit plane Corollary
- The winding number is the increment of a continuous argument divided by 2π Corollary
- The disc algebra is unital and separating but not self-adjoint or dense Counterexample
- Balls, polydiscs and the distinguished boundary in ℂᵐ Definition
- C star algebra Definition
- Complex Lp classes and Euclidean test-function conventions Definition
- Continuous logarithms and continuous arguments along a contour Definition
- Integrable real and complex functions, and their integrals Definition
- Real and complex inner product spaces, with the inner product linear in the first argument Definition
- Real and complex inner-product spaces and their induced length Definition
- Real Givens rotations and complex Givens transformations Definition
- Self-adjoint complex function algebras, unitality, and point separation Definition
- Square-summable families on an arbitrary index set and the space ℓ²(I) Definition
- Stolz approach regions at the boundary point 1 of the unit disc Definition
- The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral Definition
- The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane Definition
- The Frobenius norm ‖ A‖_F=(∑_i,j|aᵢⱼ|²)^1/2 on real or complex matrices Definition
- The standard inner product on cf(G) Definition
- The unit disc, the upper half-plane, and Blaschke factors Definition
- Wirtinger operators in ℂᵐ Definition
- {1+i, 1-i} is a normal basis of ℂ/ℝ while {1,i} is not Example
- A continuous argument computed along a spiralling contour Example
- Continuous kernel integral operator is compact on c of an interval Example
- Fredholm alternative for an integral equation Example
- The power series of exp(z₀+z₁) on every bidisc Example
- The standard inner products make K n, ell two and quotient L two Hilbert spaces Example
- The unit circle traversed three times has index 3 at every interior point Example
- Trigonometric polynomials are uniformly dense on the unit circle Example
- Unitary and special unitary Lie groups Example
- FALSE: real differentiability as a map ℝ²→ℝ² implies complex differentiability; conjugation is the counterexample False statement
- A disc missing p carries a holomorphic logarithm of z-p Lemma
- A real-linear functional on ℂᵐ is complex linear exactly when its antiholomorphic part vanishes Lemma
- An algebraic-integer average of roots of unity is either 0 or a common root of unity Lemma
- Canonical Banach complexification of a real Banach space Lemma
- Clarkson inequalities in both exponent ranges Lemma
- Conjugation is an involutive real-field automorphism, zz̄=|z|², and modulus is definite, multiplicative, and subadditive Lemma
- Equality in the unit-complex finite-sum bound Lemma
…and 21 more results.
Dependency tree · two levels
18 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, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)