Mathlib Map

Theorems · Definition · logic and foundations

FirstOrder.Field.compatibleRingOfModelField

(K : Type u_2) →
  [inst : FirstOrder.Language.ring.Structure K] →
    [inst_1 : K ⊨ FirstOrder.Language.Theory.field] → FirstOrder.Ring.CompatibleRing K

The instances given by fieldOfModelField are compatible with the Language.ring.Structure instance on K. This instance is to be used on models for the language of fields that do not already have the ring operations on the Type. Always add fieldOfModelField as a local instance first before using this instance.

Defined in
Mathlib.ModelTheory.Algebra.Field.Basic
Cited by
3 results in Mathlib
Foundations
Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FirstOrder.Language.StructureFirstOrder.Language.Theory.Model
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

FirstOrder.Field.ACF_isComplete · cited by 3Field.ACF_isCompleteFirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize · cited by 2Field.finite_ACF_prime_no…FirstOrder.Field.ACF_categorical · cited by 1Field.ACF_categoricalFirstOrder.Language.Structure · cited by 775Language.StructureFirstOrder.Language.Theory.Model · cited by 67Theory.ModelFirstOrder.Language.ring · cited by 36Language.ringFirstOrder.Ring.CompatibleRing · cited by 27Ring.CompatibleRingFirstOrder.Language.Theory.field · cited by 6Theory.fieldFirstOrder.Field.fieldOfModelField · cited by 0Field.fieldOfModelFieldFirstOrder.Ring.compatibleRingOfRingStructure · cited by 0Ring.compatibleRingOfRing…Field.compatibleRingOfModelFi…CITED BYCITES

Cites7

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

Cited by3

Results whose statement or proof uses this declaration.