theorem CoxeterGroup.conjugation_reflection_identity {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (w u : W) (s : B) (v : B → ℝ) : have α := ((coxeterRepresentation M cs) u) (e s); have s_α := u * cs.simple s * u⁻¹; have β := ((coxeterRepresentation M cs) w) α; ((coxeterRepresentation M cs) (w * s_α * w⁻¹)) v = generalizedReflection M β v

Section 1.6 conjugacy identity: with $\alpha = u \cdot \alpha_s$, $s_\alpha = u s_s u^{-1}$, and $\beta = w \cdot \alpha$, one has $w s_\alpha w^{-1} = s_\beta$ as operators on $\mathbb{R}^B$.