Theorems · Theorem · logic and foundations

FirstOrder.Ring.CompatibleRing.funMap_mul

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

Multiplication in the Language.ring.Structure is the same as the multiplication given by the Mul 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