Inversion

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

Statistics

Metric	Count
Definitions `IsLeftInversion`, `IsReflection`, `IsRightInversion`, `leftInvSeq`, `rightInvSeq`	5
Theorems `nodup_leftInvSeq`, `nodup_rightInvSeq`, `conj`, `inv`, `isLeftInversion_mul_right_iff`, `isReflection_inv`, `isRightInversion_mul_left_iff`, `length_mul_left_ne`, `length_mul_right_ne`, `mul_self`, `not_isLeftInversion_mul_right_iff`, `not_isRightInversion_mul_left_iff`, `odd_length`, `pow_two`, `getD_leftInvSeq`, `getD_leftInvSeq_mul_self`, `getD_leftInvSeq_mul_wordProd`, `getD_rightInvSeq`, `getD_rightInvSeq_mul_self`, `getElem_leftInvSeq`, `getElem_leftInvSeq_alternatingWord`, `getElem_rightInvSeq`, `getElem_succ_leftInvSeq_alternatingWord`, `isLeftInversion_inv_iff`, `isLeftInversion_of_mem_leftInvSeq`, `isLeftInversion_simple_iff_isLeftDescent`, `isReflection_conj_iff`, `isReflection_of_mem_leftInvSeq`, `isReflection_of_mem_rightInvSeq`, `isReflection_simple`, `isRightInversion_inv_iff`, `isRightInversion_of_mem_rightInvSeq`, `isRightInversion_simple_iff_isRightDescent`, `leftInvSeq_concat`, `leftInvSeq_nil`, `leftInvSeq_reverse`, `leftInvSeq_singleton`, `leftInvSeq_take`, `length_leftInvSeq`, `length_rightInvSeq`, `prod_leftInvSeq`, `prod_rightInvSeq`, `rightInvSeq_concat`, `rightInvSeq_drop`, `rightInvSeq_nil`, `rightInvSeq_reverse`, `rightInvSeq_singleton`, `wordProd_mul_getD_rightInvSeq`	48
Total	53

CoxeterSystem

Definitions

Name	Category	Theorems
`IsLeftInversion` 📖	MathDef	6 math math: `IsReflection.isLeftInversion_mul_right_iff`, `isLeftInversion_simple_iff_isLeftDescent`, `isLeftInversion_inv_iff`, `isLeftInversion_of_mem_leftInvSeq`, `IsReflection.not_isLeftInversion_mul_right_iff`, `isRightInversion_inv_iff`
`IsReflection` 📖	MathDef	4 math math: `isReflection_of_mem_rightInvSeq`, `isReflection_simple`, `isReflection_conj_iff`, `isReflection_of_mem_leftInvSeq`
`IsRightInversion` 📖	MathDef	6 math math: `isRightInversion_of_mem_rightInvSeq`, `isLeftInversion_inv_iff`, `IsReflection.not_isRightInversion_mul_left_iff`, `IsReflection.isRightInversion_mul_left_iff`, `isRightInversion_simple_iff_isRightDescent`, `isRightInversion_inv_iff`
`leftInvSeq` 📖	CompOp	15 math math: `getElem_leftInvSeq_alternatingWord`, `leftInvSeq_reverse`, `getD_leftInvSeq`, `prod_leftInvSeq`, `getElem_succ_leftInvSeq_alternatingWord`, `getD_leftInvSeq_mul_self`, `leftInvSeq_concat`, `rightInvSeq_reverse`, `leftInvSeq_nil`, `leftInvSeq_singleton`, `leftInvSeq_take`, `length_leftInvSeq`, `getD_leftInvSeq_mul_wordProd`, `IsReduced.nodup_leftInvSeq`, `getElem_leftInvSeq`
`rightInvSeq` 📖	CompOp	13 math math: `leftInvSeq_reverse`, `IsReduced.nodup_rightInvSeq`, `rightInvSeq_singleton`, `rightInvSeq_reverse`, `getD_rightInvSeq_mul_self`, `rightInvSeq_concat`, `rightInvSeq_nil`, `length_rightInvSeq`, `getElem_rightInvSeq`, `wordProd_mul_getD_rightInvSeq`, `prod_rightInvSeq`, `rightInvSeq_drop`, `getD_rightInvSeq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getD_leftInvSeq` 📖	mathematical	—	`leftInvSeq` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `wordProd` `simple` `InvOneClass.toInv`	—	`Nat.instCanonicallyOrderedAdd` `wordProd_nil` `mul_one` `inv_one` `length_leftInvSeq` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `one_mul` `inv_simple` `simple_mul_simple_self` `List.getD_map` `wordProd_cons` `mul_inv_rev`
`getD_leftInvSeq_mul_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `leftInvSeq` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`getD_leftInvSeq` `mul_assoc` `em` `inv_mul_cancel` `one_mul` `simple_mul_simple_self` `mul_inv_cancel` `mul_one`
`getD_leftInvSeq_mul_wordProd` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `leftInvSeq` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `wordProd`	—	`getD_leftInvSeq` `lt_or_ge` `mul_assoc` `wordProd_append` `wordProd_singleton` `inv_mul_cancel_left` `simple_mul_simple_cancel_left` `mul_one` `mul_inv_cancel` `one_mul`
`getD_rightInvSeq` 📖	mathematical	—	`rightInvSeq` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `wordProd` `simple`	—	`Nat.instCanonicallyOrderedAdd` `wordProd_nil` `inv_one` `mul_one` `length_rightInvSeq` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `zero_add`
`getD_rightInvSeq_mul_self` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `rightInvSeq` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`getD_rightInvSeq` `mul_assoc` `em` `mul_inv_cancel` `one_mul` `simple_mul_simple_self` `inv_mul_cancel` `mul_one`
`getElem_leftInvSeq` 📖	mathematical	—	`leftInvSeq` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `wordProd` `simple` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`List.getD_eq_getElem` `getD_leftInvSeq`
`getElem_leftInvSeq_alternatingWord` 📖	mathematical	—	`leftInvSeq` `alternatingWord` `wordProd`	—	`length_alternatingWord` `getElem_leftInvSeq` `wordProd_nil` `one_mul` `inv_one` `mul_one` `wordProd_singleton` `getElem_alternatingWord` `add_zero` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `getElem_succ_leftInvSeq_alternatingWord` `inv_simple` `alternatingWord_succ'` `wordProd_cons` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `alternatingWord_succ` `wordProd_concat` `mul_assoc`
`getElem_rightInvSeq` 📖	mathematical	—	`rightInvSeq` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `wordProd` `simple` `InvOneClass.toOne`	—	`List.getD_eq_getElem` `getD_rightInvSeq`
`getElem_succ_leftInvSeq_alternatingWord` 📖	mathematical	—	`leftInvSeq` `alternatingWord` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MonoidHom` `MulAut` `MulAut.instGroup` `MonoidHom.instFunLike` `MulAut.conj` `simple`	—	`length_alternatingWord` `getElem_leftInvSeq` `listTake_succ_alternatingWord` `wordProd_cons` `mul_assoc` `mul_inv_rev` `inv_simple` `LeftCancelSemigroup.toIsLeftCancelMul` `RightCancelSemigroup.toIsRightCancelMul` `getElem_alternatingWord_swapIndices`
`isLeftInversion_inv_iff` 📖	mathematical	—	`IsLeftInversion` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `IsRightInversion`	—	`inv_inv` `isRightInversion_inv_iff`
`isLeftInversion_of_mem_leftInvSeq` 📖	mathematical	`IsReduced` `leftInvSeq`	`IsLeftInversion` `wordProd`	—	`isReflection_of_mem_leftInvSeq` `List.getD_eq_getElem` `getD_leftInvSeq_mul_wordProd` `length_wordProd_le` `List.length_eraseIdx_add_one` `length_leftInvSeq` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`isLeftInversion_simple_iff_isLeftDescent` 📖	mathematical	—	`IsLeftInversion` `simple` `IsLeftDescent`	—	`isReflection_simple`
`isReflection_conj_iff` 📖	mathematical	—	`IsReflection` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_mul_cancel` `one_mul` `inv_inv` `inv_mul_cancel_right` `IsReflection.conj`
`isReflection_of_mem_leftInvSeq` 📖	mathematical	`leftInvSeq`	`IsReflection`	—	`isReflection_of_mem_rightInvSeq`
`isReflection_of_mem_rightInvSeq` 📖	mathematical	`rightInvSeq`	`IsReflection`	—	`mul_one` `neg_neg` `zpow_one`
`isReflection_simple` 📖	mathematical	—	`IsReflection` `simple`	—	`one_mul` `inv_one` `mul_one`
`isRightInversion_inv_iff` 📖	mathematical	—	`IsRightInversion` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `IsLeftInversion`	—	`length_inv` `mul_inv_rev` `inv_inv` `IsReflection.inv`
`isRightInversion_of_mem_rightInvSeq` 📖	mathematical	`IsReduced` `rightInvSeq`	`IsRightInversion` `wordProd`	—	`isReflection_of_mem_rightInvSeq` `List.getD_eq_getElem` `wordProd_mul_getD_rightInvSeq` `length_wordProd_le` `List.length_eraseIdx_add_one` `length_rightInvSeq` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`isRightInversion_simple_iff_isRightDescent` 📖	mathematical	—	`IsRightInversion` `simple` `IsRightDescent`	—	`isReflection_simple`
`leftInvSeq_concat` 📖	mathematical	—	`leftInvSeq` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `wordProd` `simple` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`wordProd_reverse` `inv_inv`
`leftInvSeq_nil` 📖	mathematical	—	`leftInvSeq`	—	—
`leftInvSeq_reverse` 📖	mathematical	—	`leftInvSeq` `rightInvSeq`	—	—
`leftInvSeq_singleton` 📖	mathematical	—	`leftInvSeq` `simple`	—	—
`leftInvSeq_take` 📖	mathematical	—	`leftInvSeq`	—	`rightInvSeq_drop` `length_rightInvSeq`
`length_leftInvSeq` 📖	mathematical	—	`leftInvSeq`	—	`length_rightInvSeq`
`length_rightInvSeq` 📖	mathematical	—	`rightInvSeq`	—	—
`prod_leftInvSeq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `leftInvSeq` `InvOneClass.toInv` `wordProd`	—	`List.prod_reverse_noncomm` `IsReflection.inv` `isReflection_of_mem_rightInvSeq` `wordProd_reverse` `prod_rightInvSeq`
`prod_rightInvSeq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `rightInvSeq` `InvOneClass.toInv` `wordProd`	—	`wordProd_nil` `inv_one` `mul_inv_cancel_right` `wordProd_cons` `mul_inv_rev` `inv_simple`
`rightInvSeq_concat` 📖	mathematical	—	`rightInvSeq` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MonoidHom` `MulAut` `MulAut.instGroup` `MonoidHom.instFunLike` `MulAut.conj` `simple`	—	`rightInvSeq_singleton` `wordProd_append` `wordProd_cons` `wordProd_nil` `mul_one` `mul_inv_rev` `inv_simple`
`rightInvSeq_drop` 📖	mathematical	—	`rightInvSeq`	—	`rightInvSeq.eq_2`
`rightInvSeq_nil` 📖	mathematical	—	`rightInvSeq`	—	—
`rightInvSeq_reverse` 📖	mathematical	—	`rightInvSeq` `leftInvSeq`	—	—
`rightInvSeq_singleton` 📖	mathematical	—	`rightInvSeq` `simple`	—	`wordProd_nil` `inv_one` `one_mul` `mul_one`
`wordProd_mul_getD_rightInvSeq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `wordProd` `rightInvSeq` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`getD_rightInvSeq` `lt_or_ge` `wordProd_append` `mul_assoc` `wordProd_singleton` `mul_inv_cancel_left` `simple_mul_simple_cancel_left` `mul_one` `inv_mul_cancel`

CoxeterSystem.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nodup_leftInvSeq` 📖	mathematical	`CoxeterSystem.IsReduced`	`CoxeterSystem.leftInvSeq`	—	`nodup_rightInvSeq` `CoxeterSystem.isReduced_reverse_iff`
`nodup_rightInvSeq` 📖	mathematical	`CoxeterSystem.IsReduced`	`CoxeterSystem.rightInvSeq`	—	`List.nodup_iff_getElem?_ne_getElem?` `CoxeterSystem.length_rightInvSeq` `List.getD_eq_getElem` `Option.some_injective` `CoxeterSystem.getD_rightInvSeq_mul_self` `mul_assoc` `mul_one` `CoxeterSystem.wordProd_mul_getD_rightInvSeq` `CoxeterSystem.length_wordProd_le`

CoxeterSystem.IsReflection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj` 📖	mathematical	`CoxeterSystem.IsReflection`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_zpow_neg_one`
`inv` 📖	mathematical	`CoxeterSystem.IsReflection`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_assoc` `mul_inv_rev` `inv_inv` `CoxeterSystem.inv_simple`
`isLeftInversion_mul_right_iff` 📖	mathematical	`CoxeterSystem.IsReflection`	`CoxeterSystem.IsLeftInversion` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`CoxeterSystem.isRightInversion_inv_iff` `mul_inv_rev` `inv` `isRightInversion_mul_left_iff`
`isReflection_inv` 📖	mathematical	`CoxeterSystem.IsReflection`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`isRightInversion_mul_left_iff` 📖	mathematical	`CoxeterSystem.IsReflection`	`CoxeterSystem.IsRightInversion` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul_assoc` `mul_self` `mul_one` `le_of_lt` `lt_of_le_of_ne'` `length_mul_left_ne`
`length_mul_left_ne` 📖	—	`CoxeterSystem.IsReflection`	—	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `CoxeterSystem.lengthParity_simple` `map_inv` `mul_inv_cancel_comm` `Multiplicative.isLeftCancelMul` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NeZero.one` `ZMod.nontrivial` `Nat.Prime.one_lt'` `Nat.fact_prime_two` `Mathlib.Tactic.Contrapose.contrapose₄` `CoxeterSystem.lengthParity_eq_ofAdd_length`
`length_mul_right_ne` 📖	—	`CoxeterSystem.IsReflection`	—	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `CoxeterSystem.lengthParity_simple` `map_inv` `mul_inv_cancel_comm` `Multiplicative.isRightCancelMul` `AddRightCancelSemigroup.toIsRightCancelAdd` `NeZero.one` `ZMod.nontrivial` `Nat.Prime.one_lt'` `Nat.fact_prime_two` `Mathlib.Tactic.Contrapose.contrapose₄` `CoxeterSystem.lengthParity_eq_ofAdd_length`
`mul_self` 📖	mathematical	`CoxeterSystem.IsReflection`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`conj_mul` `CoxeterSystem.simple_mul_simple_self` `mul_one` `mul_inv_cancel`
`not_isLeftInversion_mul_right_iff` 📖	mathematical	`CoxeterSystem.IsReflection`	`CoxeterSystem.IsLeftInversion` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Iff.not_left` `isLeftInversion_mul_right_iff`
`not_isRightInversion_mul_left_iff` 📖	mathematical	`CoxeterSystem.IsReflection`	`CoxeterSystem.IsRightInversion` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Iff.not_left` `isRightInversion_mul_left_iff`
`odd_length` 📖	mathematical	`CoxeterSystem.IsReflection`	`Odd` `Nat.instSemiring` `CoxeterSystem.length`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `CoxeterSystem.lengthParity_simple` `map_inv` `mul_inv_cancel_comm` `CoxeterSystem.lengthParity_eq_ofAdd_length` `EquivLike.toEmbeddingLike`
`pow_two` 📖	mathematical	`CoxeterSystem.IsReflection`	`Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`conj_pow` `CoxeterSystem.simple_sq` `mul_one` `mul_inv_cancel`

---

← Back to Index