degree_eq_one_of_irreducible — Mathlib

English

If p ∈ k[X] is irreducible and separable over a separably closed k, then deg p = 1.

Русский

Если p ∈ k[X] неразложим и сепарабельен над сепарабельным замкнутым полем k, то deg p = 1.

LaTeX

$$Irreducible p → Separable p → p.degree = 1$$

Lean4

theorem degree_eq_one_of_irreducible [IsSepClosed k] {p : k[X]} (hp : Irreducible p) (hsep : p.Separable) :
    p.degree = 1 :=
  degree_eq_one_of_irreducible_of_splits hp (IsSepClosed.splits_codomain p hsep)

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