commutatorMap

Mathlib.GroupTheory.FixedPointFree

URI: https://scilib.ai/kg/mathlib#MonoidHom.commutatorMap

Lean4

/-- The commutator map `g ↦ g / φ g`. If `φ g = h * g * h⁻¹`, then `g / φ g` is exactly the
  commutator `[g, h] = g * h * g⁻¹ * h⁻¹`. -/
def commutatorMap [Div G] (g : G) :=
  g / φ g

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

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

Разделы

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

Аффилиация

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