genericMonicPolyHasRoot — Mathlib

English

The equality expressing that a generic monic polynomial has a root is equivalent to the existential property of evaluation of the monic polynomial, under the relabeled term, in the field theory.

Русский

Равенство, выражающее наличие корня у общего монического многочлена, эквивалентно существующему свойству оценки монического полинома в поле.

LaTeX

$$genericMonicPolyHasRoot(n) = ((termOfFreeCommRing (genericMonicPoly n)).relabel Sum.inr = 0).ex.alls eq_1$$

Lean4

/-- A sentence saying every monic polynomial of degree `n` has a root. -/
noncomputable def genericMonicPolyHasRoot (n : ℕ) : Language.ring.Sentence :=
  (∃'((termOfFreeCommRing (genericMonicPoly n)).relabel Sum.inr =' 0)).alls

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