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{Z}[X])$$$
Lean4
theorem X_pow_sub_X_sub_one_irreducible (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 hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by simp only [trinomial, C_neg, C_1]; ring
rw [hp]
apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩
rintro z ⟨h1, h2⟩
apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z
rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2
simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C, Units.val_neg, Units.val_one, map_neg,
map_one] at h1 h2
replace h1 : z ^ n = z + 1 := by linear_combination h1
replace h2 := mul_eq_zero_of_left h2 z
rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ, Nat.sub_add_cancel hn.le] at h2
rw [h1] at h2 ⊢
exact ⟨rfl, by linear_combination -h2⟩
