Theorems · Theorem · logic and foundations

FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp

∀ {K : Type u_2} [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K]
  [inst_5 : FirstOrder.Ring.CompatibleRing K] (ax : FirstOrder.Field.FieldAxiom),
  K ⊨ ax.toSentence ↔ FirstOrder.Field.FieldAxiom.toProp K ax

Defined in: Mathlib.ModelTheory.Algebra.Field.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Add Mul Neg Zero One FirstOrder.Ring.CompatibleRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

Fin.snocproof · cited by 113
FirstOrder.Language.Sentence.Realizestatement · cited by 62
FirstOrder.Language.ringstatement · cited by 36
FirstOrder.Ring.CompatibleRingstatement and proof · cited by 27
FirstOrder.Field.FieldAxiomstatement and proof · cited by 11
FirstOrder.Ring.realize_zeroproof · cited by 5
FirstOrder.Field.FieldAxiom.toPropstatement · cited by 2
Fin.castPred_oneproof · cited by 1
FirstOrder.Ring.realize_addproof · cited by 1
FirstOrder.Ring.realize_mulproof · cited by 1
FirstOrder.Ring.realize_negproof · cited by 1
FirstOrder.Ring.realize_oneproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Field.FieldAxiom.toProp_of_modelproof · cited by 0