reindex — Mathlib

English

Reindexing a Coxeter system via a bijection of index sets yields a new Coxeter system which is isomorphic to the original one, via the reindexing isomorphism.

Русский

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

LaTeX

$$$\text{CoxeterSystem}(M,e) \cong \text{CoxeterSystem}(M) $$$

Lean4

/-- Reindex a Coxeter system through a bijection of the indexing sets. -/
@[simps]
protected def reindex (e : B ≃ B') : CoxeterSystem (M.reindex e) W :=
  ⟨cs.mulEquiv.trans (M.reindexGroupEquiv e).symm⟩

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