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

[trivial1711]

• 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

[trivial1711]

Hello, I'm currently working on simplifying the proofs and improving the API.

[trivial1711]

Hello, I'm done simplifying the proofs. The PR is dependent on #11493 now, though.

[trivial1711]

I realized while revising this pull request that I had left two different ways to get simple reflections of a Coxeter system: the FunLike instance and the function simpleReflection. I slightly modified the code so everything is written in terms of the simpleReflection function and there is no FunLike instance, because I don't think that the FunLike instance is very intuitive.

[trivial1711]

Thanks for the feedback, I'll take care of this tomorrow.

[trivial1711]

I realized today that the names of a lot of the theorems in the original file GroupTheory.Coxeter.Basic should be changed, so I went ahead and did it. I changed the PR description to describe exactly what I changed.

[trivial1711]

I am going to split this into two pull requests to make it easier to review.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11493~~
• ~~leanprover-community/mathlib4#11804~~
• ~~leanprover-community/mathlib4#11836~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style