English
For z ∈ C and n ∈ N, it is not the case that z^n = z + 1 and z^n + z^2 = 0 simultaneously.
Русский
Для произвольного z ∈ ℂ и n ∈ ℕ не существует одновременного выполнения условий z^n = z + 1 и z^n + z^2 = 0.
LaTeX
$$$\\forall z \\in \\mathbb{C}, \\ \\forall n \\in \\mathbb{N},\\; \\neg\\bigl(z^n = z+1 \\land z^n + z^2 = 0\\bigr)$$$
Lean4
theorem X_pow_sub_X_sub_one_irreducible_aux (z : ℂ) : ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0) :=
by
rintro ⟨h1, h2⟩
replace h3 : z ^ 3 = 1 := by linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2
have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2 :=
by
rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
interval_cases n % 3 <;> simp only [pow_zero, pow_one, or_true, true_or]
have z_ne_zero : z ≠ 0 := fun h =>
zero_ne_one ((zero_pow three_ne_zero).symm.trans (show (0 : ℂ) ^ 3 = 1 from h ▸ h3))
rcases key with (key | key | key)
· exact z_ne_zero (by rwa [key, right_eq_add] at h1)
· exact one_ne_zero (by rwa [key, left_eq_add] at h1)
· exact z_ne_zero (pow_eq_zero (by rwa [key, add_self_eq_zero] at h2))
