English
Let K be a field equipped with a compatible ring structure. For every natural number n, the assertion that the generic monic polynomial of degree n has a root in K is logically equivalent to the statement that every monic polynomial over K of degree n has a root in K.
Русский
Пусть K — поле с совместимой кольцевой структурой. Для каждого натурального числа n утверждение о существовании корня у обобщённого мономного полинома степени n над K эквивалентно утверждению, что любой мономный полином над K степени n имеет корень в K.
LaTeX
$$$K \vDash \text{genericMonicPolyHasRoot}(n) \;\Longleftrightarrow\; \forall p : \{ p : K[X] \;\text{---}\; p.Monic \wedge p.natDegree = n \}, \exists x \; p.1.eval\ x = 0$$$
Lean4
theorem realize_genericMonicPolyHasRoot [Field K] [CompatibleRing K] (n : ℕ) :
K ⊨ genericMonicPolyHasRoot n ↔ ∀ p : { p : K[X] // p.Monic ∧ p.natDegree = n }, ∃ x, p.1.eval x = 0 :=
by
let _ := Classical.decEq K
rw [Equiv.forall_congr_left ((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv)]
simp [Sentence.Realize, genericMonicPolyHasRoot, lift_genericMonicPoly]
