Theorems · Theorem · logic and foundations

FirstOrder.Ring.CompatibleRing.funMap_zero

∀ {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 0 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0

The constant 0 in the Language.ring.Structure is the same as the constant given by the Zero instance

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

FirstOrder.Ring.CompatibleRing