mulOfRingStructure

Mathlib.ModelTheory.Algebra.Ring.Basic

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

Lean4

/-- 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` -/
abbrev mulOfRingStructure : Mul R :=
  { mul := fun x y => funMap mulFunc ![x, y] }

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

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

Разделы

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

Аффилиация

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