Theorems · Theorem · group theory

CoxeterSystem.reindex_simple

∀ {B : Type u_1} {B' : Type u_2} (e : B ≃ B') {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B}
  (cs : CoxeterSystem M W) (i' : B'), (cs.reindex e).simple i' = cs.simple (e.symm i')

Defined in

Mathlib.GroupTheory.Coxeter.Basic

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group