Theorems · Definition · logic and foundations
FirstOrder.Language.Theory.field
FirstOrder.Language.ring.Theory
The first-order theory of fields, as a theory over the language of rings
- Defined in
- Mathlib.ModelTheory.Algebra.Field.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.rangeproof · cited by 4,705
- FirstOrder.Language.Theorystatement · cited by 154
- FirstOrder.Language.ringstatement · cited by 36
- FirstOrder.Field.FieldAxiom.toSentenceproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- FirstOrder.Field.ACF_isCompleteproof · cited by 3
- FirstOrder.Field.compatibleRingOfModelFieldstatement and proof · cited by 3
- FirstOrder.Field.fieldOfModelACFproof · cited by 3
- FirstOrder.Field.modelField_of_modelACFstatement · cited by 3
- FirstOrder.Language.Theory.fieldOfCharproof · cited by 2
- FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realizeproof · cited by 2
- FirstOrder.Field.ACF_categoricalproof · cited by 1
- FirstOrder.Field.charP_iff_model_fieldOfCharproof · cited by 1
- FirstOrder.Field.fieldOfModelFieldstatement and proof · cited by 0
- FirstOrder.Field.FieldAxiom.toProp_of_modelstatement and proof · cited by 0