Basic

📁 Source: Mathlib/ModelTheory/Algebra/Field/Basic.lean

Statistics

Metric	Count
Definitions FieldAxiom, toProp, toSentence, compatibleRingOfModelField, fieldOfModelField	5
Theorems realize_toSentence_iff_toProp, toProp_of_model, instModelField	3
Total	8

FirstOrder.Field

Definitions

Name	Category	Theorems
FieldAxiom 📖	CompData	—
compatibleRingOfModelField 📖	CompOp	—
fieldOfModelField 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instModelField 📖	mathematical	—	FirstOrder.Language.Theory.Model FirstOrder.Language.ring FirstOrder.Ring.CompatibleRing.toStructure Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass FirstOrder.Language.Theory.field	—	FieldAxiom.realize_toSentence_iff_toProp add_assoc zero_add neg_add_cancel mul_assoc mul_comm one_mul mul_inv_cancel₀ mul_add Distrib.leftDistribClass exists_pair_ne DivisionRing.toNontrivial

FirstOrder.Field.FieldAxiom

Definitions

Name	Category	Theorems
toProp 📖	MathDef	2 math math: realize_toSentence_iff_toProp, toProp_of_model
toSentence 📖	CompOp	1 math math: realize_toSentence_iff_toProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realize_toSentence_iff_toProp 📖	mathematical	—	FirstOrder.Language.Sentence.Realize FirstOrder.Language.ring FirstOrder.Ring.CompatibleRing.toStructure toSentence toProp	—	Empty.instIsEmpty Fin.isEmpty' FirstOrder.Ring.realize_add IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instCharZero Fin.castPred_one FirstOrder.Ring.realize_zero FirstOrder.Ring.realize_neg Zero.instNonempty FirstOrder.Ring.realize_mul FirstOrder.Ring.realize_one
toProp_of_model 📖	mathematical	—	toProp	—	realize_toSentence_iff_toProp FirstOrder.Language.Theory.realize_sentence_of_mem Set.mem_range_self

---

← Back to Index