Over an algebraically closed field, an irreducible homogeneous binary form has degree one. The affine chart reduces this to a univariate polynomial.
theorem
CCDN.binary_homogeneous_irreducible_degree_le_one
{K : Type u_1}
[Field K]
[IsAlgClosed K]
{d : ℕ}
(f : MvPolynomial (Fin 2) K)
(hf : f.IsHomogeneous d)
(hir : Irreducible f)
:
Over an algebraically closed field, an irreducible homogeneous polynomial in two variables
has degree at most 1.