Cauchy–Riemann equations

TheoremComplex conjugation is nowhere complex-differentiable#●ready to prove

Let \(f : \mathbb{C} \to \mathbb{C}\) be the function \(f(z) = \bar z\). Then \(f\) is not complex-differentiable at any point \(z \in \mathbb{C}\).

public theorem_wanted not_differentiableAt_conj (f : ℂ → ℂ) (hf : ∀ z : ℂ, f z = conj z) :
    ∀ z : ℂ, ¬ DifferentiableAt ℂ f z

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_57.

TheoremA holomorphic function with holomorphic conjugate is constant#●ready to prove

Let \(U \subseteq \mathbb{C}\) be a connected open set and let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on \(U\). If the conjugate function \(z \mapsto \overline{f(z)}\) is also holomorphic on \(U\), then \(f\) is constant on \(U\): there is \(c \in \mathbb{C}\) with \(f(z) = c\) for all \(z \in U\).

public theorem_wanted exists_eqOn_const_of_differentiableOn_conj
    {U : Set ℂ} (hUopen : IsOpen U) (hUconn : IsConnected U)
    (f : ℂ → ℂ)
    (hf : DifferentiableOn ℂ f U)
    (hconj : DifferentiableOn ℂ (fun z => conj (f z)) U) :
    ∃ c : ℂ, Set.EqOn f (fun _ => c) U

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_04.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.