simple_mul_simple_self — Mathlib

English

The simple reflections satisfy the relation s_i^2 = 1 in the Coxeter group.

Русский

Пусть отражения удовлетворяют отношению s_i^2 = 1 в группе Коксетера.

LaTeX

$$$s_i^2 = 1$$$

Lean4

@[simp]
theorem simple_mul_simple_self (i : B) : s i * s i = 1 :=
  by
  have : (FreeGroup.of i) * (FreeGroup.of i) ∈ M.relationsSet := ⟨(i, i), by simp [relation]⟩
  have : (PresentedGroup.mk _ (FreeGroup.of i * FreeGroup.of i) : M.Group) = 1 :=
    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)
  unfold simple
  rw [← map_mul, PresentedGroup.of, map_mul]
  exact map_mul_eq_one cs.mulEquiv.symm this

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