exists_root_C_mul_X_pow_add_C_mul_X_add_C'

English

In a separably closed field k of characteristic p, if p divides n and n ≥ 2 and b ≠ 0, there exists x ∈ k with a x^n + b x + c = 0.

Русский

В сепарабельном замкнутом поле kchar p, если p делит n и n≥2, а b ≠ 0, то существует x ∈ k такое, что a x^n + b x + c = 0.

LaTeX

$$$p \mid n \wedge 2 \le n \wedge b \neq 0 \Rightarrow \exists x\in k:\ a x^n + b x + c = 0$$$

Lean4

/-- If a separably closed field `k` is of characteristic `p`, `n ≥ 2` is such that `p ∣ n`, `b ≠ 0`,
then there exists `x` in `k` such that `a * x ^ n + b * x + c = 0`. -/
theorem exists_root_C_mul_X_pow_add_C_mul_X_add_C' [IsSepClosed k] (p n : ℕ) (a b c : k) [CharP k p] (hn : p ∣ n)
    (hn' : 2 ≤ n) (hb : b ≠ 0) : ∃ x, a * x ^ n + b * x + c = 0 :=
  exists_root_C_mul_X_pow_add_C_mul_X_add_C a b c ((CharP.cast_eq_zero_iff k p n).2 hn) hn' hb

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