theorem AffineReflectionGroup.stabilizer_linearPart_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) (w₁ : E ≃ᵃⁱ[ℝ] E) : w₁ ∈ W.Stabilizer x → ∀ w₂ ∈ W.Stabilizer x, linearPartHom w₁ = linearPartHom w₂ → w₁ = w₂

For an affine reflection group $W$ and a point $x ∈ E$, the linear-part homomorphism $\mathrm{linearPartHom}$ is injective on the stabilizer of $x$: two stabilizing isometries with the same linear part are equal.