IsReflection

Mathlib.GroupTheory.Coxeter.Inversion

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.IsReflection

← MathLib Explorer

English

Each simple reflection s_i is a reflection of the Coxeter system.

Русский

Каждое простое отражение s_i является отражением системы Коксетера.

LaTeX

$$$cs.IsReflection (s_i)$$$

Lean4

/-- `t : W` is a *reflection* of the Coxeter system `cs` if it is of the form
$w s_i w^{-1}$, where $w \in W$ and $s_i$ is a simple reflection. -/
def IsReflection (t : W) : Prop :=
  ∃ w i, t = w * s i * w⁻¹

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

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

Разделы

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

Аффилиация

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