mathlib4 feat: the Chebyshev polynomials C and S

We define the rescaled Chebyshev polynomials $C_n$ and $S_n$ (also known as the Vieta–Lucas and Vieta–Fibonacci polynomials, respectively). They are related to the Chebyshev polynomials $T_n$ and $U_n$ by the formulas $C_n(2x) = 2T_n(x)$ and $S_n(2x) = U_n(x)$. Most theorems about $T_n$ and $U_n$ have analogues involving $C_n$ and $S_n$.

We prove that $C_n$ and $S_n$ are special cases of the Dickson polynomials (though unlike general Dickson polynomials, they are defined for every integer $n$, not just natural numbers).

These polynomials are necessary to state a formula for $(r_1 r_2)^m v$, where $v \in V$ is an element of a module, $r_1, r_2 \in GL(V)$ are reflections, and $m$ is an integer. The formula will be used to define and construct reflection representations of a Coxeter group over an arbitrary commutative ring, not necessarily having an invertible 2. See #13291.

[x] depends on: #13133

May 25 '24 06:05 trivial1711

This PR/issue depends on:

~~leanprover-community/mathlib4#13133~~ By Dependent Issues (🤖). Happy coding!

May 28 '24 14:05 leanprover-community-mathlib4-bot

PR summary ce36390104

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

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_mul_C + 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_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 + T_mul_T + 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

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).