feat: add simple reflections, words, lifting to Coxeter groups

[trivial1711]

trafficstars

• Move all material about Coxeter groups from GroupTheory/SpecificGroups to GroupTheory/Coxeter.
• Slightly change the definition of a Coxeter system so the associated matrix actually needs to be a Coxeter matrix.
• Rename theorem AₙIsCoxeter to isCoxeter_Aₙ to follow Mathlib naming conventions, and similarly for similar theorems.
• Update docstrings of GroupTheory/Coxeter/Basic.lean to include a note about what happens when an entry of the Coxeter matrix is zero.
• Add definitions CoxeterSystem.simpleReflection, CoxeterSystem.lift, and CoxeterSystem.wordProd to GroupTheory/Coxeter/Basic.lean and prove their basic properties.

---

• [x] depends on: #11493