Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 00:37 7fb7fb36

View on Github →

feat(ring_theory/polynomial/chebyshev/dickson): Introduce generalised Dickson polynomials (#5869) and replace lambdashev with dickson 1 1.

Estimated changes

Modified docs/references.bib

Modified src/ring_theory/polynomial/chebyshev/basic.lean

added theorem polynomial.chebyshev₁_eq_dickson_one_one

deleted theorem polynomial.chebyshev₁_eq_lambdashev

added theorem polynomial.dickson_one_one_char_p

added theorem polynomial.dickson_one_one_comp_comm

added theorem polynomial.dickson_one_one_eq_chebyshev₁

added theorem polynomial.dickson_one_one_eval_add_inv

added theorem polynomial.dickson_one_one_mul

added theorem polynomial.dickson_one_one_zmod_p

deleted theorem polynomial.lambdashev_char_p

deleted theorem polynomial.lambdashev_comp_comm

deleted theorem polynomial.lambdashev_eq_chebyshev₁

deleted theorem polynomial.lambdashev_eval_add_inv

deleted theorem polynomial.lambdashev_mul

deleted theorem polynomial.lambdashev_zmod_p

Modified src/ring_theory/polynomial/chebyshev/defs.lean

deleted theorem polynomial.lambdashev_add_two

deleted theorem polynomial.lambdashev_eq_two_le

deleted theorem polynomial.lambdashev_one

deleted theorem polynomial.lambdashev_two

deleted theorem polynomial.lambdashev_zero

deleted theorem polynomial.map_lambdashev

Created src/ring_theory/polynomial/chebyshev/dickson.lean

added theorem polynomial.dickson_add_two

added theorem polynomial.dickson_of_two_le

added theorem polynomial.dickson_one

added theorem polynomial.dickson_two

added theorem polynomial.dickson_two_zero

added theorem polynomial.dickson_zero

added theorem polynomial.map_dickson