Theorems · Theorem · logic and foundations

FirstOrder.Field.realize_genericMonicPolyHasRoot

∀ {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K] (n : ℕ),
  K ⊨ FirstOrder.Field.genericMonicPolyHasRoot n ↔
    ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, Polynomial.eval x ↑p = 0

Defined in: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Cited by: 1 results in Mathlib
Foundations: Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field FirstOrder.Ring.CompatibleRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Fieldstatement and proof · cited by 7,404
Polynomialstatement · cited by 5,681
Equiv.symmproof · cited by 3,681
LinearEquiv.symmproof · cited by 1,461
Polynomial.natDegreestatement · cited by 1,105
Polynomial.evalstatement and proof · cited by 796
Polynomial.Monicstatement · cited by 461
Equiv.transproof · cited by 337
Fin.snocproof · cited by 113
LinearEquiv.toEquivproof · cited by 105
FirstOrder.Language.Sentence.Realizestatement and proof · cited by 62

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Field.isAlgClosed_of_model_ACFproof · cited by 2