loopOfHom

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

URI: https://scilib.ai/kg/mathlib#IsFreeGroupoid.SpanningTree.loopOfHom

← MathLib Explorer

English

A spanning tree provides canonical loops; the loop relations hold identity.

Русский

Дерево связности даёт канонические петли; петли равны тождеству.

LaTeX

$$loopOfHom_eq_id$$

Lean4

/-- Any hom in `G` can be made into a loop, by conjugating with `treeHom`s. -/
def loopOfHom {a b : G} (p : a ⟶ b) : End (root' T) :=
  treeHom T a ≫ p ≫ inv (treeHom T b)

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

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

Разделы

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

Аффилиация

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