addOfRingStructure

Mathlib.ModelTheory.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Ring.addOfRingStructure

Lean4

/-- A def to put an `Add` 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` -/
abbrev addOfRingStructure : Add R :=
  { add := fun x y => funMap addFunc ![x, y] }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru