Theorems · Theorem · commutative algebra

Polynomial.Chebyshev.C_mul

∀ (R : Type u_1) [inst : CommRing R] (m n : ℤ),
  Polynomial.Chebyshev.C R (m * n) = (Polynomial.Chebyshev.C R m).comp (Polynomial.Chebyshev.C R n)

The (m * n)-th Chebyshev C polynomial is the composition of the m-th and n-th.

Defined in

Mathlib.RingTheory.Polynomial.Chebyshev

Cited by

0 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing