EnvelGroup

Mathlib.Algebra.Quandle

URI: https://scilib.ai/kg/mathlib#Rack.EnvelGroup

Lean4

/-- The universal enveloping group for the rack R.
-/
def EnvelGroup (R : Type*) [Rack R] :=
  Quotient
    (PreEnvelGroup.setoid R)
      -- Define the `Group` instances in two steps so `inv` can be inferred correctly.
      -- TODO: is there a non-invasive way of defining the instance directly?

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

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

Разделы

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

Аффилиация

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