Kadiri.riemannZeta_order_conj

theorem riemannZeta_order_conj {ρ : ℂ} (hρ : ρ ≠ 1) :    riemannZeta.order ((starRingEnd ℂ) ρ) = riemannZeta.order ρ := by  have hρ' : (starRingEnd ℂ) ρ ≠ 1 := by    intro h    apply hρ    have := congrArg (starRingEnd ℂ) h    simpa [Complex.conj_conj] using this  have han : AnalyticAt ℂ riemannZeta ρ :=    riemannZeta_analyticOn_compl_one ρ (by simpa [Set.mem_compl_iff] using hρ)  have han' : AnalyticAt ℂ riemannZeta ((starRingEnd ℂ) ρ) :=    riemannZeta_analyticOn_compl_one _ (by simpa [Set.mem_compl_iff] using hρ')  have hfun : (fun w ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) w))) = riemannZeta := by    funext w    rw [riemannZeta_conj, Complex.conj_conj]  have hkey := analyticOrderAt_conj_conj (f := riemannZeta)    (z₀ := (starRingEnd ℂ) ρ) (by simpa [Complex.conj_conj] using han)  rw [hfun, Complex.conj_conj] at hkey  unfold riemannZeta.order  rw [han.meromorphicOrderAt_eq, han'.meromorphicOrderAt_eq, hkey]