Commit 2023-05-26 08:39 4667c8af

View on Github →

feat: port RingTheory.Polynomial.Dickson (#4382) Rewrote the proof for dickson_one_one_eq_chebyshev_T and chebyshev_T_eq_dickson_one_one

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Dickson.lean

added theorem Polynomial.chebyshev_T_eq_dickson_one_one

added theorem Polynomial.dickson_add_two

added theorem Polynomial.dickson_of_two_le

added theorem Polynomial.dickson_one

added theorem Polynomial.dickson_one_one_charP

added theorem Polynomial.dickson_one_one_comp_comm

added theorem Polynomial.dickson_one_one_eq_chebyshev_T

added theorem Polynomial.dickson_one_one_eval_add_inv

added theorem Polynomial.dickson_one_one_mul

added theorem Polynomial.dickson_one_one_zmod_p

added theorem Polynomial.dickson_two

added theorem Polynomial.dickson_two_zero

added theorem Polynomial.dickson_zero

added theorem Polynomial.map_dickson