Theorems · Definition · logic and foundations
FirstOrder.Field.genericMonicPolyHasRoot
ℕ → FirstOrder.Language.ring.Sentence
A sentence saying every monic polynomial of degree n has a root.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Language.Sentencestatement · cited by 127
- FirstOrder.Language.ringstatement · cited by 36
- FirstOrder.Language.Term.relabelproof · cited by 27
- FirstOrder.Language.BoundedFormula.exproof · cited by 14
- FirstOrder.Language.Term.bdEqualproof · cited by 10
- FirstOrder.Ring.termOfFreeCommRingproof · cited by 5
- FirstOrder.Language.BoundedFormula.allsproof · cited by 2
- FirstOrder.Field.genericMonicPolyproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Theory.ACFproof · cited by 11
- FirstOrder.Field.modelField_of_modelACFproof · cited by 3
- FirstOrder.Field.isAlgClosed_of_model_ACFproof · cited by 2
- FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realizeproof · cited by 2
- FirstOrder.Field.realize_genericMonicPolyHasRootstatement and proof · cited by 1