Remark

Tag 0ALQ, permanent. Cite it as [Bourbaki, Tag 0ALQ].

Lie Groups and Lie Algebras, chapter IV, § 1. Coxeter Groups

In view of formulas (1) and (2), the formula $d(w, w') = l(w{w'}^{-1})$ defines a distance on $W$ , invariant under right translations.

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.

Cited by

Nothing.

Nothing.