theorem deriv_conj_conj' (f : ℂ → ℂ) (p : ℂ) : deriv (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) ((starRingEnd ℂ) p) = (starRingEnd ℂ) (deriv f p)

theorem deriv_riemannZeta_conj (s : ℂ) : deriv riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (deriv riemannZeta s)

theorem logDerivZeta_conj (s : ℂ) : (deriv riemannZeta / riemannZeta) ((starRingEnd ℂ) s) = (starRingEnd ℂ) ((deriv riemannZeta / riemannZeta) s)

theorem logDerivZeta_conj' (s : ℂ) : logDeriv riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (logDeriv riemannZeta s)

theorem intervalIntegral_conj {f : ℝ → ℂ} {a b : ℝ} : ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (f x) = (starRingEnd ℂ) (∫ (x : ℝ) in a..b, f x)