IsLeftInversion

Mathlib.GroupTheory.Coxeter.Inversion

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

← MathLib Explorer

English

A left inversion is a reflection t with ℓ(t w) < ℓ(w).

Русский

Левое инвертирование — это отражение t с ℓ(t w) < ℓ(w).

LaTeX

$$$cs.IsLeftInversion\, w\, t \iff cs.IsReflection t \land \ell(t w) < \ell w$$$

Lean4

/-- The proposition that `t` is a left inversion of `w`; i.e., `t` is a reflection and
$\ell (t w) < \ell(w)$. -/
def IsLeftInversion (w t : W) : Prop :=
  cs.IsReflection t ∧ ℓ(t * w) < ℓ w

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

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

Разделы

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

Аффилиация

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