Fundamental theorem of algebra

import Mathlib

theorem fund_theorem_algebra (p : Polynomial ℂ) (h : 0 < p.degree) : ∃ z, p.eval z = 0 :=by
  rcases Complex.exists_root h with ⟨z, hz⟩
  exact ⟨z, hz⟩