root_exists — Mathlib

English

Over an algebraically closed field k of characteristic p, for any n, a1, a2 with nonzero 0th coefficients, there exists b ∈ k such that succNthDefiningPoly(p,n,a1,a2,bs) has b as a root.

Русский

Пусть k — замкнутое в алгебре поле характеристикой p; для любых n и Witt-векторов a1,a2 с ненулевой 0-й компонентой существует b ∈ k, такой что succNthDefiningPoly(p,n,a1,a2,bs) имеет корень b.

LaTeX

$$$\exists b \in k,\; (\operatorname{succNthDefiningPoly}(p,n,a_1,a_2,bs)).IsRoot(b)$$$

Lean4

theorem root_exists (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
    ∃ b : k, (succNthDefiningPoly p n a₁ a₂ bs).IsRoot b :=
  IsAlgClosed.exists_root _ <| by
    simp only [succNthDefiningPoly_degree p n a₁ a₂ bs ha₁ ha₂, ne_eq, Nat.cast_eq_zero, hp.out.ne_zero,
      not_false_eq_true]

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