Commit 2025-10-07 09:26 51d6a5ed

View on Github →

refactor: Chebyshev: avoid reducing wfrec (#30290)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/Chebyshev.lean

modified theorem Polynomial.Chebyshev.C_neg_one

modified theorem Polynomial.Chebyshev.C_one

modified theorem Polynomial.Chebyshev.C_zero

modified theorem Polynomial.Chebyshev.S_one

modified theorem Polynomial.Chebyshev.S_zero

modified theorem Polynomial.Chebyshev.T_neg_one

modified theorem Polynomial.Chebyshev.T_one

modified theorem Polynomial.Chebyshev.T_zero

modified theorem Polynomial.Chebyshev.U_one

modified theorem Polynomial.Chebyshev.U_zero