Theorems · Definition · logic and foundations

FirstOrder.Ring.oneOfRingStructure

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

A def to put an One 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 10 from the axioms · uses no axioms

Assumes

FirstOrder.Language.Structure