English
Let n ∈ ℕ with n ≠ 1. Then the polynomial X^n − X − 1 in ℚ[X] is irreducible.
Русский
Пусть n ∈ ℕ и 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
theorem X_pow_sub_X_sub_one_irreducible_rat (hn1 : n ≠ 1) : Irreducible (X ^ n - X - 1 : ℚ[X]) :=
by
by_cases hn0 : n = 0
· rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by simp only [trinomial, C_neg, C_1]; ring
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp (X_pow_sub_X_sub_one_irreducible hn1)
· rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one, Polynomial.map_X] at h
· exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive
