Theorems · Theorem · logic and foundations

FirstOrder.Ring.realize_one

∀ {α : 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] (v : α → R), FirstOrder.Language.Term.realize v 1 = 1

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

AddMulNegOneZeroFirstOrder.Ring.CompatibleRing