Theorems · Theorem · logic and foundations

FirstOrder.Ring.CompatibleRing.funMap_neg

∀ {R : Type u_2} {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R}
  [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 1 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0

Negation in the Language.ring.Structure is the same as the negation given by the Neg instance

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

2 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

FirstOrder.Ring.CompatibleRing