Length

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

Statistics

Metric	Count
Definitions IsLeftDescent, IsReduced, IsRightDescent, length, lengthParity	5
Theorems drop, reverse, take, 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_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	37
Total	42

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	3 math math: not_isReduced_alternatingWord, 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	20 math math: length_eq_one_iff, length_mul_le, length_mul_simple, length_mul_ge_length_sub_length', length_simple_mul, length_one, length_mul_ge_max, not_isLeftDescent_iff, length_wordProd_le, isLeftDescent_iff, exists_reduced_word, 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_leftDescent_of_ne_one 📖	mathematical	—	IsLeftDescent	—	exists_reduced_word wordProd_nil IsLeftDescent.eq_1 wordProd_cons simple_mul_simple_cancel_left length_wordProd_le IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass
exists_reduced_word 📖	mathematical	—	length wordProd	—	Nat.find_spec
exists_reduced_word' 📖	mathematical	—	IsReduced wordProd	—	exists_reduced_word
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_reduced_word 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_reduced_word wordProd_singleton length_simple
length_eq_zero_iff 📖	mathematical	—	length InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	exists_reduced_word wordProd_nil length_one
length_inv 📖	mathematical	—	length InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	exists_reduced_word length_wordProd_le wordProd_reverse inv_inv
length_mul_ge_length_sub_length 📖	mathematical	—	length MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Nat.instOrderedSub 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	—	Nat.instOrderedSub add_comm inv_mul_cancel_left length_inv length_mul_le
length_mul_ge_max 📖	mathematical	—	length MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	max_le_iff 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_reduced_word length_wordProd_le 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	—	length_mul_simple_ne length_mul_ge_length_sub_length length_simple Nat.instOrderedSub 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 📖	—	—	—	—	mul_inv_rev inv_simple inv_inv length_inv 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 📖	—	CoxeterSystem.IsReduced	—	—	—
reverse 📖	—	CoxeterSystem.IsReduced	—	—	CoxeterSystem.isReduced_reverse_iff
take 📖	—	CoxeterSystem.IsReduced	—	—	—

---

← Back to Index