Theorems · Theorem · group theory
CoxeterMatrix.reindex_relationsSet
∀ {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B ≃ B'),
(CoxeterMatrix.reindex e M).relationsSet = ⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet- Defined in
- Mathlib.GroupTheory.Coxeter.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- Equivstatement and proof · cited by 8,337
- Set.imagestatement and proof · cited by 5,609
- Set.rangeproof · cited by 4,705
- SProd.sprodproof · cited by 1,750
- MulEquivstatement · cited by 1,142
- map_mulproof · cited by 1,137
- Set.image_congrproof · cited by 533
- map_powproof · cited by 503
- Set.image_univproof · cited by 322
- Equiv.symm_apply_applyproof · cited by 320
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.