toNonAssocRing

Mathlib.Algebra.Ring.Defs

URI: https://scilib.ai/kg/mathlib#Ring.toNonAssocRing

English

As a ring, α carries a nonassociative ring structure.

Русский

Как кольцо, α имеет структуру неассоциированного кольца.

LaTeX

$$$Ring(\alpha) \to NonAssocRing(\alpha)$$$

Lean4

instance (priority := 100) toNonAssocRing : NonAssocRing α :=
  { ‹Ring α› with }

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

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

Разделы

Аффилиация

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