submonoid_closure_range_simple — Mathlib

English

The simple reflections generate the Coxeter group W as a group; equivalently the subgroup generated by the range of simple is all of W.

Русский

Простые отражения порождают группу W как группу; эквивалентно тому, что подгруппа, порождённая диапазоном простых отражений, равна всей W.

LaTeX

$$Subgroup.closure( range cs.simple ) = ⊤$$

Lean4

/-- The simple reflections of `W` generate `W` as a monoid. -/
theorem submonoid_closure_range_simple : Submonoid.closure (range cs.simple) = ⊤ :=
  by
  have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by simp_rw [inv_range, inv_simple, union_self]
  rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]

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