Length

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

Statistics

Metric	Count
Definitions `IsLeftDescent`, `IsReduced`, `IsRightDescent`, `length`, `lengthParity`	5
Theorems `drop`, `eq`, `reverse`, `take`, `exists_isReduced`, `exists_leftDescent_of_ne_one`, `exists_reduced_word`, `exists_reduced_word'`, `exists_rightDescent_of_ne_one`, `isLeftDescent_iff`, `isLeftDescent_iff_not_isLeftDescent_mul`, `isLeftDescent_inv_iff`, `isReduced_reverse_iff`, `isRightDescent_iff`, `isRightDescent_iff_not_isRightDescent_mul`, `isRightDescent_inv_iff`, `lengthParity_comp_simple`, `lengthParity_eq_ofAdd_length`, `lengthParity_simple`, `length_eq_one_iff`, `length_eq_zero_iff`, `length_inv`, `length_le_length_mul_add_left`, `length_le_length_mul_add_right`, `length_mul_ge_length_sub_length`, `length_mul_ge_length_sub_length'`, `length_mul_ge_max`, `length_mul_le`, `length_mul_mod_two`, `length_mul_simple`, `length_mul_simple_ne`, `length_one`, `length_simple`, `length_simple_mul`, `length_simple_mul_ne`, `length_wordProd_le`, `not_isLeftDescent_iff`, `not_isLeftDescent_one`, `not_isReduced_alternatingWord`, `not_isRightDescent_iff`, `not_isRightDescent_one`	41
Total	46

CoxeterSystem

Definitions

Name	Category	Theorems
`IsLeftDescent` 📖	MathDef	8 math math: `not_isLeftDescent_one`, `not_isLeftDescent_iff`, `isLeftDescent_iff`, `isRightDescent_inv_iff`, `isLeftInversion_simple_iff_isLeftDescent`, `exists_leftDescent_of_ne_one`, `isLeftDescent_inv_iff`, `isLeftDescent_iff_not_isLeftDescent_mul`
`IsReduced` 📖	MathDef	8 math math: `not_isReduced_alternatingWord`, `IsReduced.drop`, `exists_isReduced`, `IsReduced.take`, `exists_reduced_word`, `IsReduced.reverse`, `exists_reduced_word'`, `isReduced_reverse_iff`
`IsRightDescent` 📖	MathDef	8 math math: `exists_rightDescent_of_ne_one`, `isRightDescent_inv_iff`, `isRightDescent_iff_not_isRightDescent_mul`, `isRightInversion_simple_iff_isRightDescent`, `isRightDescent_iff`, `not_isRightDescent_one`, `isLeftDescent_inv_iff`, `not_isRightDescent_iff`
`length` 📖	CompOp	22 math math: `length_eq_one_iff`, `length_mul_le`, `length_mul_simple`, `length_le_length_mul_add_left`, `length_mul_ge_length_sub_length'`, `IsReduced.eq`, `length_simple_mul`, `length_one`, `length_mul_ge_max`, `not_isLeftDescent_iff`, `length_wordProd_le`, `isLeftDescent_iff`, `length_le_length_mul_add_right`, `isRightDescent_iff`, `lengthParity_eq_ofAdd_length`, `not_isRightDescent_iff`, `length_simple`, `length_eq_zero_iff`, `IsReflection.odd_length`, `length_mul_mod_two`, `length_inv`, `length_mul_ge_length_sub_length`
`lengthParity` 📖	CompOp	3 math math: `lengthParity_comp_simple`, `lengthParity_simple`, `lengthParity_eq_ofAdd_length`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isReduced` 📖	mathematical	—	`IsReduced` `wordProd`	—	`Nat.find_spec`
`exists_leftDescent_of_ne_one` 📖	mathematical	—	`IsLeftDescent`	—	`exists_isReduced` `wordProd_nil` `IsLeftDescent.eq_1` `wordProd_cons` `simple_mul_simple_cancel_left` `length_wordProd_le` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd`
`exists_reduced_word` 📖	mathematical	—	`IsReduced` `wordProd`	—	`exists_isReduced`
`exists_reduced_word'` 📖	mathematical	—	`IsReduced` `wordProd`	—	`exists_isReduced`
`exists_rightDescent_of_ne_one` 📖	mathematical	—	`IsRightDescent`	—	`exists_leftDescent_of_ne_one`
`isLeftDescent_iff` 📖	mathematical	—	`IsLeftDescent` `length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`length_simple_mul`
`isLeftDescent_iff_not_isLeftDescent_mul` 📖	mathematical	—	`IsLeftDescent` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`isLeftDescent_iff` `not_isLeftDescent_iff` `simple_mul_simple_cancel_left`
`isLeftDescent_inv_iff` 📖	mathematical	—	`IsLeftDescent` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `IsRightDescent`	—	`length_inv` `mul_inv_rev` `inv_inv` `inv_simple`
`isReduced_reverse_iff` 📖	mathematical	—	`IsReduced`	—	`wordProd_reverse` `length_inv`
`isRightDescent_iff` 📖	mathematical	—	`IsRightDescent` `length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`length_mul_simple`
`isRightDescent_iff_not_isRightDescent_mul` 📖	mathematical	—	`IsRightDescent` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`isRightDescent_iff` `not_isRightDescent_iff` `simple_mul_simple_cancel_right`
`isRightDescent_inv_iff` 📖	mathematical	—	`IsRightDescent` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `IsLeftDescent`	—	`inv_inv` `isLeftDescent_inv_iff`
`lengthParity_comp_simple` 📖	mathematical	—	`Multiplicative` `ZMod` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `MonoidHom.instFunLike` `lengthParity` `simple` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `AddMonoidWithOne.toOne`	—	`lengthParity_simple`
`lengthParity_eq_ofAdd_length` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `ZMod` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `MonoidHom.instFunLike` `lengthParity` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `AddMonoidWithOne.toNatCast` `length`	—	`exists_isReduced` `wordProd.eq_1` `map_list_prod` `MonoidHom.instMonoidHomClass` `lengthParity_comp_simple` `List.prod_replicate` `ofAdd_nsmul` `nsmul_one`
`lengthParity_simple` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `ZMod` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `MonoidHom.instFunLike` `lengthParity` `simple` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `AddMonoidWithOne.toOne`	—	`lift_apply_simple`
`length_eq_one_iff` 📖	mathematical	—	`length` `simple`	—	`exists_isReduced` `wordProd_singleton` `length_simple`
`length_eq_zero_iff` 📖	mathematical	—	`length` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`exists_isReduced` `wordProd_nil` `length_one`
`length_inv` 📖	mathematical	—	`length` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`exists_isReduced` `length_wordProd_le` `wordProd_reverse` `inv_inv`
`length_le_length_mul_add_left` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`add_comm` `inv_mul_cancel_left` `length_inv` `length_mul_le`
`length_le_length_mul_add_right` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul_inv_cancel_right` `length_inv` `length_mul_le`
`length_mul_ge_length_sub_length` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`length_le_length_mul_add_right`
`length_mul_ge_length_sub_length'` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`length_le_length_mul_add_left`
`length_mul_ge_max` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`max_le` `length_mul_ge_length_sub_length` `length_mul_ge_length_sub_length'`
`length_mul_le` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`exists_isReduced` `length_wordProd_le` `IsReduced.eq` `wordProd_append`
`length_mul_mod_two` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`ZMod.natCast_eq_natCast_iff'` `Nat.cast_add` `lengthParity_eq_ofAdd_length` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`length_mul_simple` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`Ne.lt_or_gt` `length_mul_simple_ne` `LE.le.antisymm` `length_simple` `length_le_length_mul_add_right` `LE.le.antisymm'` `length_mul_le`
`length_mul_simple_ne` 📖	—	—	—	—	`length_mul_mod_two` `length_simple`
`length_one` 📖	mathematical	—	`length` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`length_wordProd_le`
`length_simple` 📖	mathematical	—	`length` `simple`	—	`wordProd_singleton` `zero_add` `length_wordProd_le` `lengthParity_eq_ofAdd_length` `Nat.cast_zero` `lengthParity_simple`
`length_simple_mul` 📖	mathematical	—	`length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`length_mul_simple` `length_inv` `mul_inv_rev` `inv_simple`
`length_simple_mul_ne` 📖	—	—	—	—	`length_inv` `mul_inv_rev` `inv_simple` `length_mul_simple_ne`
`length_wordProd_le` 📖	mathematical	—	`length` `wordProd`	—	`Nat.find_min'`
`not_isLeftDescent_iff` 📖	mathematical	—	`IsLeftDescent` `length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`length_simple_mul`
`not_isLeftDescent_one` 📖	mathematical	—	`IsLeftDescent` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_one` `length_simple` `length_one` `Nat.instCanonicallyOrderedAdd`
`not_isReduced_alternatingWord` 📖	mathematical	`CoxeterMatrix.M`	`IsReduced` `alternatingWord`	—	`le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `prod_alternatingWord_eq_prod_alternatingWord_sub` `length_wordProd_le` `length_alternatingWord` `Mathlib.Tactic.Contrapose.contrapose₄` `IsReduced.drop` `alternatingWord_succ'`
`not_isRightDescent_iff` 📖	mathematical	—	`IsRightDescent` `length` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `simple`	—	`length_mul_simple`
`not_isRightDescent_one` 📖	mathematical	—	`IsRightDescent` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`one_mul` `length_simple` `length_one` `Nat.instCanonicallyOrderedAdd`

CoxeterSystem.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`drop` 📖	mathematical	`CoxeterSystem.IsReduced`	`CoxeterSystem.IsReduced`	—	—
`eq` 📖	mathematical	`CoxeterSystem.IsReduced`	`CoxeterSystem.length` `CoxeterSystem.wordProd`	—	—
`reverse` 📖	mathematical	`CoxeterSystem.IsReduced`	`CoxeterSystem.IsReduced`	—	`CoxeterSystem.isReduced_reverse_iff`
`take` 📖	mathematical	`CoxeterSystem.IsReduced`	`CoxeterSystem.IsReduced`	—	—

---

← Back to Index