Complex.Hadamard.hadamard_factorization_of_order

theorem hadamard_factorization_of_order {f : ℂ → ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ)    (hnot : ∃ z : ℂ, f z ≠ 0)    (horder : EntireOfOrderAtMost ρ f) :    ∃ (P : Polynomial ℂ),      P.degree ≤ Nat.floor ρ ∧      ∀ z : ℂ,        f z =          Complex.exp (Polynomial.eval z P) *            z ^ (analyticOrderNatAt f 0) *            divisorCanonicalProduct (Nat.floor ρ) f (Set.univ : Set ℂ) z := by  classical  let hentire : Differentiable ℂ f := horder.differentiable  set m : ℕ := Nat.floor ρ  rcases Real.exists_between_self_and_floor_add_one_same_floor hρ with    ⟨τ, hτ, hτ_lt, hτ_nonneg, hfloorτ'⟩  have hfloorτ : Nat.floor τ = m := by    simpa [m] using hfloorτ'  have hgrowthτ :      ∃ C' > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C' * (1 + ‖z‖) ^ τ :=    horder.exists_log_growth hτ hτ_nonneg  rcases hadamard_factorization_of_growth (f := f) (ρ := τ) hτ_nonneg      hentire hnot hgrowthτ with    ⟨P, hdeg, hfac⟩  refine ⟨P, ?_, ?_⟩  · simpa [m, hfloorτ] using hdeg  · intro z    simpa [m, hfloorτ] using hfac z