Documentation

LeanPool.CCDN.Algebra.BinaryHomogeneousIrreducibility

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) :
d ≤ 1

Over an algebraically closed field, an irreducible homogeneous polynomial in two variables has degree at most 1.