succNthVal_spec — Mathlib

English

A secondary lemma detailing a congruence or equality used in proving the main polynomial identity for succNthDefiningPoly.

Русский

Вторая лемма, описывающая конгруэнцию или равенство, используемое при доказательстве основного тождества succNthDefiningPoly.

LaTeX

$$succNthDefiningPoly_eq2(p,n,a1,a2,bs) = ...$$

Lean4

theorem succNthVal_spec (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
    (succNthDefiningPoly p n a₁ a₂ bs).IsRoot (succNthVal p n a₁ a₂ bs ha₁ ha₂) :=
  Classical.choose_spec (root_exists p n a₁ a₂ bs ha₁ ha₂)

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