theorem hasDerivAt_conj_conj {f : ℂ → ℂ} {p a : ℂ} (hf : HasDerivAt f a p) : HasDerivAt (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) ((starRingEnd ℂ) a) ((starRingEnd ℂ) p)

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

theorem conj_riemannZeta_conj_aux1 (s : ℂ) (hs : 1 < s.re) : (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) s)) = riemannZeta s

theorem conj_riemannZeta_conj (s : ℂ) : (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) s)) = riemannZeta s

theorem riemannZeta_conj (s : ℂ) : riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)

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)