Mitchell Lee

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

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...

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

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...

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

I'm not entirely sure what happened with the CI here. It is not very clear about what went wrong.

Thank you so much for the feedback.

bors r+