Theorems · Theorem · logic and foundations

FirstOrder.Ring.realize_add

∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
  [inst_5 : FirstOrder.Ring.CompatibleRing R] (x y : FirstOrder.Language.ring.Term α) (v : α → R),
  FirstOrder.Language.Term.realize v (x + y) =
    FirstOrder.Language.Term.realize v x + FirstOrder.Language.Term.realize v y

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

Matrix.vecConsproof · cited by 852
Matrix.vecEmptyproof · cited by 832
Matrix.cons_val_fin_oneproof · cited by 225
FirstOrder.Language.Termstatement and proof · cited by 166
FirstOrder.Language.Term.realizestatement and proof · cited by 81
FirstOrder.Language.ringstatement and proof · cited by 36
FirstOrder.Ring.CompatibleRingstatement and proof · cited by 27
FirstOrder.Ring.CompatibleRing.funMap_addproof · cited by 2
FirstOrder.Language.Term.realize_functions_apply₂proof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toPropproof · cited by 1