simple_mul_simple_pow — Mathlib

English

The product of two simple reflections raised to the corresponding matrix entry equals the identity: (s_i s_j)^{M(i,j)} = 1.

Русский

Произведение двух простых отражений, возведённое в степень M(i,j), равно единице: (s_i s_j)^{M(i,j)} = 1.

LaTeX

$$$(s_i s_j)^{M(i,j)} = 1$$$

Lean4

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

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