degree_eq_one_of_irreducible — Mathlib

English

Over an algebraically closed field, every irreducible polynomial is linear.

Русский

Пусть k алгебраически замкнутое поле. Тогда каждый иррeдуцируемый многочлен над k линейный.

LaTeX

$$$[IsAlgClosed\;k] \Rightarrow \forall p : k[X], Irreducible p \rightarrow p.degree = 1$$$

Lean4

/-- If `k` is algebraically closed, then every irreducible polynomial over `k` is linear.
-/
@[stacks 09GR "(4) ⟹ (2)"]
theorem degree_eq_one_of_irreducible [IsAlgClosed k] {p : k[X]} (hp : Irreducible p) : p.degree = 1 :=
  degree_eq_one_of_irreducible_of_splits hp (IsAlgClosed.splits_codomain _)

Похожие утверждения