Basic

📁 Source: Mathlib/GroupTheory/Coxeter/Basic.lean

Statistics

Metric	Count
Definitions `IsLiftable`, `instGroupGroup`, `reindexGroupEquiv`, `relation`, `relationsSet`, `simple`, `toCoxeterSystem`, `CoxeterSystem`, `alternatingWord`, `braidWord`, `map`, `mulEquiv`, `reindex`, `simple`, `wordProd`, `IsCoxeterGroup`	16
Theorems `reindexGroupEquiv_apply_simple`, `reindexGroupEquiv_symm_apply_simple`, `reindex_relationsSet`, `toCoxeterSystem_simple`, `alternatingWord_succ`, `alternatingWord_succ'`, `ext`, `ext_iff`, `ext_simple`, `getElem_alternatingWord`, `getElem_alternatingWord_swapIndices`, `inv_simple`, `length_alternatingWord`, `lift_apply_simple`, `listTake_alternatingWord`, `listTake_succ_alternatingWord`, `map_mulEquiv`, `map_simple`, `prod_alternatingWord_eq_mul_pow`, `prod_alternatingWord_eq_prod_alternatingWord_sub`, `reindex_mulEquiv`, `reindex_simple`, `simple_determines_coxeterSystem`, `simple_induction`, `simple_induction_left`, `simple_induction_right`, `simple_mul_simple_cancel_left`, `simple_mul_simple_cancel_right`, `simple_mul_simple_pow`, `simple_mul_simple_pow'`, `simple_mul_simple_self`, `simple_sq`, `subgroup_closure_range_simple`, `submonoid_closure_range_simple`, `wordProd_append`, `wordProd_braidWord_eq`, `wordProd_concat`, `wordProd_cons`, `wordProd_nil`, `wordProd_reverse`, `wordProd_singleton`, `wordProd_surjective`, `nonempty_system`	43
Total	59

CoxeterMatrix

Definitions

Name	Category	Theorems
`IsLiftable` 📖	MathDef	—
`instGroupGroup` 📖	CompOp	5 math math: `CoxeterSystem.reindex_mulEquiv`, `toCoxeterSystem_simple`, `reindexGroupEquiv_apply_simple`, `CoxeterSystem.map_mulEquiv`, `reindexGroupEquiv_symm_apply_simple`
`reindexGroupEquiv` 📖	CompOp	3 math math: `CoxeterSystem.reindex_mulEquiv`, `reindexGroupEquiv_apply_simple`, `reindexGroupEquiv_symm_apply_simple`
`relation` 📖	CompOp	—
`relationsSet` 📖	CompOp	1 math math: `reindex_relationsSet`
`simple` 📖	CompOp	3 math math: `toCoxeterSystem_simple`, `reindexGroupEquiv_apply_simple`, `reindexGroupEquiv_symm_apply_simple`
`toCoxeterSystem` 📖	CompOp	1 math math: `toCoxeterSystem_simple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reindexGroupEquiv_apply_simple` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Group` `reindex` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `reindexGroupEquiv` `simple` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	—
`reindexGroupEquiv_symm_apply_simple` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Group` `reindex` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `reindexGroupEquiv` `simple` `Equiv` `Equiv.instEquivLike`	—	—
`reindex_relationsSet` 📖	mathematical	—	`relationsSet` `reindex` `Set.image` `FreeGroup` `DFunLike.coe` `MulEquiv` `FreeGroup.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `FreeGroup.freeGroupCongr`	—	`Set.range_comp` `Set.range_prodMap` `EquivLike.range_eq_univ` `Set.univ_prod_univ` `Set.image_univ` `Equiv.symm_apply_apply` `map_pow` `MonoidHom.instMonoidHomClass` `map_mul` `MonoidHomClass.toMulHomClass` `Set.image_congr`
`toCoxeterSystem_simple` 📖	mathematical	—	`CoxeterSystem.simple` `Group` `instGroupGroup` `toCoxeterSystem` `simple`	—	—

CoxeterSystem

Definitions

Name	Category	Theorems
`alternatingWord` 📖	CompOp	12 math math: `getElem_leftInvSeq_alternatingWord`, `not_isReduced_alternatingWord`, `getElem_alternatingWord_swapIndices`, `getElem_succ_leftInvSeq_alternatingWord`, `prod_alternatingWord_eq_prod_alternatingWord_sub`, `getElem_alternatingWord`, `prod_alternatingWord_eq_mul_pow`, `listTake_alternatingWord`, `alternatingWord_succ'`, `listTake_succ_alternatingWord`, `length_alternatingWord`, `alternatingWord_succ`
`braidWord` 📖	CompOp	1 math math: `wordProd_braidWord_eq`
`map` 📖	CompOp	2 math math: `map_mulEquiv`, `map_simple`
`mulEquiv` 📖	CompOp	3 math math: `reindex_mulEquiv`, `ext_iff`, `map_mulEquiv`
`reindex` 📖	CompOp	2 math math: `reindex_mulEquiv`, `reindex_simple`
`simple` 📖	CompOp	42 math math: `inv_simple`, `simple_mul_simple_pow`, `lift_apply_simple`, `length_eq_one_iff`, `getD_leftInvSeq`, `length_mul_simple`, `rightInvSeq_singleton`, `length_simple_mul`, `getElem_succ_leftInvSeq_alternatingWord`, `leftInvSeq_concat`, `wordProd_cons`, `subgroup_closure_range_simple`, `not_isLeftDescent_iff`, `rightInvSeq_concat`, `simple_determines_coxeterSystem`, `lengthParity_comp_simple`, `wordProd_concat`, `isLeftDescent_iff`, `getElem_rightInvSeq`, `wordProd_singleton`, `CoxeterMatrix.toCoxeterSystem_simple`, `simple_mul_simple_pow'`, `simple_sq`, `simple_mul_simple_cancel_left`, `lengthParity_simple`, `leftInvSeq_singleton`, `prod_alternatingWord_eq_mul_pow`, `isLeftInversion_simple_iff_isLeftDescent`, `isRightDescent_iff_not_isRightDescent_mul`, `isReflection_simple`, `simple_mul_simple_self`, `reindex_simple`, `isRightInversion_simple_iff_isRightDescent`, `map_simple`, `isRightDescent_iff`, `submonoid_closure_range_simple`, `not_isRightDescent_iff`, `getElem_leftInvSeq`, `isLeftDescent_iff_not_isLeftDescent_mul`, `length_simple`, `simple_mul_simple_cancel_right`, `getD_rightInvSeq`
`wordProd` 📖	CompOp	25 math math: `getElem_leftInvSeq_alternatingWord`, `getD_leftInvSeq`, `wordProd_reverse`, `prod_leftInvSeq`, `leftInvSeq_concat`, `wordProd_cons`, `prod_alternatingWord_eq_prod_alternatingWord_sub`, `isRightInversion_of_mem_rightInvSeq`, `wordProd_concat`, `length_wordProd_le`, `getElem_rightInvSeq`, `wordProd_singleton`, `exists_reduced_word`, `prod_alternatingWord_eq_mul_pow`, `wordProd_mul_getD_rightInvSeq`, `wordProd_nil`, `prod_rightInvSeq`, `getD_leftInvSeq_mul_wordProd`, `wordProd_surjective`, `isLeftInversion_of_mem_leftInvSeq`, `wordProd_braidWord_eq`, `getElem_leftInvSeq`, `wordProd_append`, `exists_reduced_word'`, `getD_rightInvSeq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternatingWord_succ` 📖	mathematical	—	`alternatingWord`	—	—
`alternatingWord_succ'` 📖	mathematical	—	`alternatingWord` `Even` `Nat.instDecidablePredEven`	—	`alternatingWord.eq_2`
`ext` 📖	—	`mulEquiv`	—	—	—
`ext_iff` 📖	mathematical	—	`mulEquiv`	—	`ext`
`ext_simple` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `simple`	—	—	`MonoidHom.eq_of_eqOn_denseM` `submonoid_closure_range_simple`
`getElem_alternatingWord` 📖	mathematical	—	`alternatingWord` `Even` `Nat.instDecidablePredEven`	—	—
`getElem_alternatingWord_swapIndices` 📖	mathematical	—	`alternatingWord`	—	`getElem_alternatingWord` `add_assoc` `Even.add_one` `Odd.add_one` `Nat.not_even_iff_odd`
`inv_simple` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `simple`	—	`eq_inv_of_mul_eq_one_right` `simple_mul_simple_self`
`length_alternatingWord` 📖	mathematical	—	`alternatingWord`	—	`zero_add`
`lift_apply_simple` 📖	mathematical	`CoxeterMatrix.IsLiftable`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `simple`	—	`Equiv.left_inv`
`listTake_alternatingWord` 📖	mathematical	—	`alternatingWord` `Even` `Nat.instDecidablePredEven`	—	`Nat.not_even_iff_odd` `Even.add_one` `length_alternatingWord` `alternatingWord_succ` `getElem_alternatingWord` `Nat.even_add` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `Odd.add_one` `Nat.odd_add`
`listTake_succ_alternatingWord` 📖	mathematical	—	`alternatingWord`	—	`listTake_alternatingWord` `Nat.not_even_iff_odd` `Even.add_one` `alternatingWord_succ'` `Odd.add_one`
`map_mulEquiv` 📖	mathematical	—	`mulEquiv` `map` `MulEquiv.trans` `CoxeterMatrix.Group` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CoxeterMatrix.instGroupGroup` `MulEquiv.symm`	—	—
`map_simple` 📖	mathematical	—	`simple` `map` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	—
`prod_alternatingWord_eq_mul_pow` 📖	mathematical	—	`wordProd` `alternatingWord` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Even` `Nat.instDecidablePredEven` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `simple` `Monoid.toNatPow`	—	`wordProd_nil` `pow_zero` `mul_one` `alternatingWord_succ'` `wordProd_cons` `Nat.instAtLeastTwoHAddOfNat` `even_iff_two_dvd` `one_mul` `Even.two_dvd`
`prod_alternatingWord_eq_prod_alternatingWord_sub` 📖	mathematical	`CoxeterMatrix.M`	`wordProd` `alternatingWord`	—	`prod_alternatingWord_eq_mul_pow` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_mul` `Int.even_or_odd'` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.isInt_add` `mul_comm` `sub_mul` `Int.instCharZero` `zpow_sub` `zpow_natCast` `simple_mul_simple_pow'` `inv_zpow` `one_mul` `mul_inv_rev` `inv_simple` `Int.not_even_iff_odd` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_ediv` `zero_add` `Mathlib.Meta.NormNum.IsInt.neg_to_eq` `Mathlib.Meta.NormNum.isInt_neg` `zpow_add` `zpow_neg` `zpow_one` `mul_one` `simple_mul_simple_self`
`reindex_mulEquiv` 📖	mathematical	—	`mulEquiv` `CoxeterMatrix.reindex` `reindex` `MulEquiv.trans` `CoxeterMatrix.Group` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CoxeterMatrix.instGroupGroup` `MulEquiv.symm` `CoxeterMatrix.reindexGroupEquiv`	—	—
`reindex_simple` 📖	mathematical	—	`simple` `CoxeterMatrix.reindex` `reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`simple_determines_coxeterSystem` 📖	mathematical	—	`CoxeterSystem` `simple`	—	`ext` `MulEquiv.toMonoidHom_injective` `ext_simple` `MulEquiv.apply_symm_apply`
`simple_induction` 📖	—	`simple` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—	`Submonoid.mem_top` `submonoid_closure_range_simple` `Submonoid.closure_induction`
`simple_induction_left` 📖	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	—	`Submonoid.mem_top` `submonoid_closure_range_simple` `Submonoid.closure_induction_left` `Set.mem_range`
`simple_induction_right` 📖	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	—	`Submonoid.mem_top` `submonoid_closure_range_simple` `Submonoid.closure_induction_right` `Set.mem_range`
`simple_mul_simple_cancel_left` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`simple_mul_simple_self` `one_mul`
`simple_mul_simple_cancel_right` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`mul_assoc` `simple_mul_simple_self` `mul_one`
`simple_mul_simple_pow` 📖	mathematical	—	`Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `simple` `CoxeterMatrix.M` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`QuotientGroup.eq_one_iff` `Subgroup.subset_normalClosure` `map_mul` `MonoidHomClass.toMulHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `map_pow` `MulEquiv.map_eq_one_iff`
`simple_mul_simple_pow'` 📖	mathematical	—	`Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `simple` `CoxeterMatrix.M` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`simple_mul_simple_pow` `CoxeterMatrix.symmetric`
`simple_mul_simple_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`CoxeterMatrix.diagonal` `pow_one` `QuotientGroup.eq_one_iff` `Subgroup.subset_normalClosure` `map_mul` `MonoidHomClass.toMulHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `PresentedGroup.of.eq_1` `map_mul_eq_one`
`simple_sq` 📖	mathematical	—	`Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`simple_mul_simple_self` `pow_two`
`subgroup_closure_range_simple` 📖	mathematical	—	`Subgroup.closure` `Set.range` `simple` `Top.top` `Subgroup` `Subgroup.instTop`	—	`Set.range_comp` `MulEquiv.coe_toMonoidHom` `MonoidHom.map_closure` `PresentedGroup.closure_range_of` `MonoidHom.range_eq_map` `MonoidHom.range_eq_top` `MulEquiv.surjective`
`submonoid_closure_range_simple` 📖	mathematical	—	`Submonoid.closure` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.range` `simple` `Top.top` `Submonoid` `Submonoid.instTop`	—	`Set.inv_range` `inv_simple` `Set.union_self` `Subgroup.closure_toSubmonoid` `subgroup_closure_range_simple` `Subgroup.top_toSubmonoid`
`wordProd_append` 📖	mathematical	—	`wordProd` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative`
`wordProd_braidWord_eq` 📖	mathematical	—	`wordProd` `braidWord`	—	`prod_alternatingWord_eq_prod_alternatingWord_sub` `Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `CoxeterMatrix.symmetric` `tsub_eq_of_eq_add` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_two`
`wordProd_concat` 📖	mathematical	—	`wordProd` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_one`
`wordProd_cons` 📖	mathematical	—	`wordProd` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	—
`wordProd_nil` 📖	mathematical	—	`wordProd` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`wordProd_reverse` 📖	mathematical	—	`wordProd` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`wordProd_nil` `inv_one` `wordProd_append` `wordProd_cons` `mul_one` `mul_inv_rev` `inv_simple` `RightCancelSemigroup.toIsRightCancelMul`
`wordProd_singleton` 📖	mathematical	—	`wordProd` `simple`	—	`mul_one`
`wordProd_surjective` 📖	mathematical	—	`wordProd`	—	`simple_induction_left` `wordProd_nil` `wordProd_cons`

IsCoxeterGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_system` 📖	mathematical	—	`CoxeterSystem`	—	—

(root)

Definitions

Name	Category	Theorems
`CoxeterSystem` 📖	CompData	2 math math: `CoxeterSystem.simple_determines_coxeterSystem`, `IsCoxeterGroup.nonempty_system`
`IsCoxeterGroup` 📖	CompData	—

---

← Back to Index