Theorems · Definition · logic and foundations

FirstOrder.Ring.compatibleRingOfRing

(R : Type u_2) →
  [inst : Add R] →
    [inst_1 : Mul R] → [inst_2 : Neg R] → [inst_3 : One R] → [inst_4 : Zero R] → FirstOrder.Ring.CompatibleRing R

Given a Type R with instances for each of the Ring operations, make a Language.ring.Structure R instance, along with a proof that the operations given by the Language.ring.Structure are the same as those given by the Add or Mul etc. instances. This definition can be used when applying a theorem about the model theory of rings to a literal ring R, by writing let _ := compatibleRingOfRing R. After this, if, for example, R is a field, then Lean will be able to find the instance for Theory.field.Model R, and it will be possible to apply theorems about the model theory of fields. This is a def and not an instance, because the path Ring => Language.ring.Structure => Ring cannot be made to commute by definition

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

3 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext

Assumes

AddMulNegOneZero