Theorems · Theorem · group theory
CoxeterSystem.getD_leftInvSeq_mul_wordProd
∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
(cs.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)- Defined in
- Mathlib.GroupTheory.Coxeter.Inversion
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- mul_assocproof · cited by 1,667
- lt_or_geproof · cited by 182
- CoxeterMatrixstatement and proof · cited by 140
- mul_inv_cancelproof · cited by 128
- CoxeterSystemstatement and proof · cited by 126
- inv_mul_cancel_leftproof · cited by 88
- CoxeterSystem.simpleproof · cited by 73
- CoxeterSystem.wordProdstatement and proof · cited by 42
- CoxeterSystem.leftInvSeqstatement · cited by 18
Cited by1
Results whose statement or proof uses this declaration.
- CoxeterSystem.isLeftInversion_of_mem_leftInvSeqproof · cited by 0