structure CoxeterGroupData.ReducedWord (C : CoxeterGroupData) (w : C.W) : Type u_1

• word : List C.W
• mem_simple (s : C.W) : s ∈ self.word → s ∈ C.simpleReflections
• prod_eq : self.word.prod = w
• length_eq : self.word.length = C.length w

theorem CoxeterGroupData.descentRefl_length_eq (C : CoxeterGroupData) (y : C.W) (hy : y ≠ 1) : C.length (C.descentRefl y * y) + 1 = C.length y

def CoxeterGroupData.IsReducedWord (C : CoxeterGroupData) (word : List C.W) : Prop

theorem CoxeterGroupData.length_mul_le (C : CoxeterGroupData) (v w : C.W) : C.length (v * w) ≤ C.length v + C.length w

theorem CoxeterGroupData.length_inv_le (C : CoxeterGroupData) (w : C.W) : C.length w⁻¹ ≤ C.length w

def WeylGroupData.weylLength {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (C : CoxeterGroupData) (rd : PositiveRootData Δ) (compat : CoxeterWeylCompatibility C rd wg) (w : wg.W) : ℕ

noncomputable def RootSystemWithReflections.inversions {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (_rs : RootSystemWithReflections rd wg) (w : wg.W) : Finset (↥Δ.𝔥 →ₗ[R] R)

structure SimpleRootData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (C : CoxeterGroupData) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (compat : CoxeterWeylCompatibility C rd wg) : Type (max (max u_1 u_2) u_3)

• simpleRoot : C.W → ↥Δ.𝔥 →ₗ[R] R
• simpleRoot_pos (s : C.W) : s ∈ C.simpleReflections → self.simpleRoot s ∈ rd.posRoots
• simpleRoot_mem (s : C.W) : s ∈ C.simpleReflections → self.simpleRoot s ∈ rs.allRoots
• simpleRoot_refl (s : C.W) : s ∈ C.simpleReflections → rs.reflection (self.simpleRoot s) = compat.ι s
• simpleRoot_injective (s₁ : C.W) : s₁ ∈ C.simpleReflections → ∀ s₂ ∈ C.simpleReflections, self.simpleRoot s₁ = self.simpleRoot s₂ → s₁ = s₂