feat: the Chebyshev polynomials C and S

[trivial1711]

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.

---

• depends on: [Merged by Bors] - feat: index Chebyshev polynomials by integers instead of natural numbers #13133

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: index Chebyshev polynomials by integers instead of natural numbers #13133
  By Dependent Issues (🤖). Happy coding!

[Ruben-VandeVelde]

Not a big fan of that proof - does something like this work?

Suggested change

	theorem C_neg_one : C R (-1) = X := (by ring : X * 2 - X = X)
	theorem C_neg_one : C R (-1) = X := by
	unfold C
	ring

[trivial1711]

It doesn't. Why don't you like the proof?

[j-loreaux]

How about show X * 2 - X = x by ring?

[github-actions]

PR summary 97e7841748

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

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>

[grunweg]

It looks like you have a merge conflict (which is why this PR does not appear in the review queue any more).
Can you merge master, please? Thanks!