hasSeparableContraction — Mathlib

English

For hn1: n ≠ 1, X^n - X - 1 is irreducible in ℚ[X].

Русский

Для hn1: n ≠ 1, X^n - X - 1 неприводим в ℚ[X].

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ n \\neq 1 \\Rightarrow \\operatorname{Irreducible}(X^n - X - 1 \\in \\mathbb{Q}[X])$$$

Lean4

/-- Every irreducible polynomial can be contracted to a separable polynomial. -/
@[stacks 09H0]
theorem _root_.Irreducible.hasSeparableContraction (q : ℕ) [hF : ExpChar F q] {f : F[X]} (irred : Irreducible f) :
    HasSeparableContraction q f := by
  cases hF
  · exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩
  · rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
    exact ⟨g, hgs, n, hge⟩

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