Theorems · Definition · field theory
Polynomial.dickson
{R : Type u_1} → [inst : CommRing R] → ℕ → R → ℕ → Polynomial Rdickson is the n-th (generalised) Dickson polynomial of the k-th kind associated to the
element a ∈ R.
- Defined in
- Mathlib.RingTheory.Polynomial.Dickson
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Polynomialstatement · cited by 5,681
Cited by19
Results whose statement or proof uses this declaration.
- Polynomial.map_dicksonstatement · cited by 3
- Polynomial.dickson_one_one_eq_chebyshev_Cstatement · cited by 2
- Polynomial.dickson_two_one_eq_chebyshev_Sstatement · cited by 2
- Polynomial.dickson_add_twostatement and proof · cited by 1
- Polynomial.dickson_one_one_eq_chebyshev_Tstatement · cited by 1
- Polynomial.dickson_one_one_eval_add_invstatement · cited by 1
- Polynomial.dickson_one_one_mulstatement and proof · cited by 1
- Polynomial.dickson_one_one_zmod_pstatement and proof · cited by 1
- Polynomial.dickson_two_zerostatement · cited by 0
- Polynomial.chebyshev_T_eq_dickson_one_onestatement · cited by 0
- Polynomial.chebyshev_U_eq_dickson_two_onestatement · cited by 0
- Polynomial.dickson.eq_defstatement and proof · cited by 0