Theorems · Definition · logic and foundations

FirstOrder.Ring.mulOfRingStructure

(R : Type u_2) → [FirstOrder.Language.ring.Structure R] → Mul R

A def to put an Mul instance on a type with a Language.ring.Structure instance. To be used sparingly, usually only when defining a more useful definition like, [Language.ring.Structure K] -> [Theory.field.Model K] -> Field K

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext

Assumes

FirstOrder.Language.Structure