map — Mathlib

English

Push a Coxeter system through a group isomorphism; the induced structure on the target is again a Coxeter system with the same matrix up to the induced equivalence.

Русский

Перемещаем систему Коксетера через изоморфизм групп; полученная структура на целевой группе снова является системой Коксетера с тем же матрицей, скорректированной соответствующим эквивалентом.

LaTeX

$$$\text{map}_e\colon \text{CoxeterSystem}(M,W) \to \text{CoxeterSystem}(M,W) \\text{(via } e\text{)}$$$

Lean4

/-- Push a Coxeter system through a group isomorphism. -/
@[simps]
protected def map (e : W ≃* H) : CoxeterSystem M H :=
  ⟨e.symm.trans cs.mulEquiv⟩

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