degree_eq_one_of_irreducible_of_splits

English

If p is an irreducible polynomial over K and splits over the identity embedding of K, then deg p = 1.

Русский

Если p — неприводимый полином над K и распадается над тождественным вложением K в себя, то степень p равна 1.

LaTeX

$$$\\forall p \\in K[X],\\; \\text{Irreducible}(p) \\land \\text{Splits}(\\mathrm{id}_K, p) \\Rightarrow \\deg(p) = 1.$$$

Lean4

theorem degree_eq_one_of_irreducible_of_splits {p : K[X]} (hp : Irreducible p) (hp_splits : Splits (RingHom.id K) p) :
    p.degree = 1 := by
  rcases hp_splits with ⟨⟩ | hp_splits
  · exfalso
    simp_all
  · apply hp_splits hp
    simp

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