feat: power of product of two reflections

[trivial1711]

Let $M$ be a module over a commutative ring $R$. Let $x, y \in M$ and $f, g \in M^*$ with $f(x) = g(y) = 2$. The corresponding reflections $r_1, r_2 \colon M \to M$ are given by $r_1z = z - f(z) x$ and $r_2 z = z - g(z) y$. These are linear automorphisms of $M$.

We prove that for all $z \in M$ and all $m \in \mathbb{Z}$, we have:
$$(r_1 r_2)^m z = z + S_{\left\lfloor \frac{m-2}{2} \right \rfloor}(t) (S_{\left\lfloor \frac{m-1}{2} \right \rfloor}(t) + S_{\left\lfloor \frac{m-3}{2} \right \rfloor}(t)) (g(x) f(z) y - g(z) y - f(z) x) + S_{\left\lfloor \frac{m-1}{2} \right \rfloor}(t) (S_{\left\lfloor \frac{m}{2} \right \rfloor}(t) + S_{\left\lfloor \frac{m-2}{2} \right \rfloor}(t)) (f(y) g(z) x - f(z) x - g(z) y)$$
$$(r_1 r_2)^m x = (S_{m}(t) + S_{m - 1}(t)) x - S_{m-1} g(x) y$$
$$r_2(r_1 r_2)^m x = (S_{m}(t) + S_{m - 1}(t)) x - S_{m} g(x) y$$
where $t = f(y) g(x) - 2$ and $S_n$ refers to a Chebyshev $S$-polynomial.

These formulas may look ridiculous, but they are necessary for constructing reflection representations of a Coxeter group over an arbitrary ring. See #13291 for more details.

---

• depends on: feat: the Chebyshev polynomials C and S #13195
  

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• feat: the Chebyshev polynomials C and S #13195
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Would you mind copying your appendix to a github issue, and then linking to that issue from here?
I think that is a better location for this explanation, because then it can be linked to from multiple locations.

[trivial1711]

Would you mind copying your appendix to a github issue, and then linking to that issue from here? I think that is a better location for this explanation, because then it can be linked to from multiple locations.

Thanks for the suggestion. I have done it: #13291

[github-actions]

PR summary 6c62c04c86

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Reflection	1140	1141	+1 (+0.09%)

---

Declarations diff

+ C
+ C_add_one
+ C_add_two
+ C_comp_two_mul_X
+ C_eq
+ C_eq_S_sub_X_mul_S
+ C_eq_two_mul_T_comp_half_mul_X
+ C_mul
+ C_natAbs
+ C_neg
+ C_neg_one
+ C_neg_two
+ C_one
+ C_sub_one
+ C_sub_two
+ C_two
+ C_two_mul_complex_cos
+ C_two_mul_real_cos
+ C_zero
+ S
+ S_add_one
+ S_add_two
+ S_comp_two_mul_X
+ S_eq
+ S_eq_U_comp_half_mul_X
+ S_eq_X_mul_S_add_C
+ S_neg
+ S_neg_one
+ S_neg_sub_one
+ S_neg_sub_two
+ S_neg_two
+ S_one
+ S_sq_add_S_sq
+ S_sub_one
+ S_sub_two
+ S_two
+ S_two_mul_complex_cos
+ S_two_mul_real_cos
+ S_zero
+ T_eq_half_mul_C_comp_two_mul_X
+ chebyshev_U_eq_dickson_two_one
+ dickson_one_one_eq_chebyshev_C
+ dickson_two_one_eq_chebyshev_S
+ dickson_two_one_eq_chebyshev_U
+ map_C
+ map_S
+ mul_C
+ mul_apply
+ reflection_inv
+ reflection_mul_reflection_mul_reflection_pow_apply_self
+ reflection_mul_reflection_mul_reflection_zpow_apply_self
+ reflection_mul_reflection_pow_apply
+ reflection_mul_reflection_pow_apply_self
+ reflection_mul_reflection_zpow_apply
+ reflection_mul_reflection_zpow_apply_self

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>