Dickson

📁 Source: Mathlib/RingTheory/Polynomial/Dickson.lean

Statistics

Metric	Count
Definitions dickson	1
Theorems chebyshev_T_eq_dickson_one_one, chebyshev_U_eq_dickson_two_one, dickson_add_two, dickson_of_two_le, dickson_one, dickson_one_one_charP, dickson_one_one_comp_comm, dickson_one_one_eq_chebyshev_C, dickson_one_one_eq_chebyshev_T, dickson_one_one_eval_add_inv, dickson_one_one_mul, dickson_one_one_zmod_p, dickson_two, dickson_two_one_eq_chebyshev_S, dickson_two_one_eq_chebyshev_U, dickson_two_zero, dickson_zero, map_dickson	18
Total	19

Polynomial

Definitions

Name	Category	Theorems
dickson 📖	CompOp	18 math math: map_dickson, dickson_one_one_mul, dickson_two_one_eq_chebyshev_S, dickson_two_zero, chebyshev_U_eq_dickson_two_one, dickson_one_one_eq_chebyshev_C, dickson_one_one_comp_comm, dickson_add_two, dickson_one_one_charP, dickson_one_one_zmod_p, dickson_one_one_eq_chebyshev_T, chebyshev_T_eq_dickson_one_one, dickson_of_two_le, dickson_zero, dickson_two_one_eq_chebyshev_U, dickson_two, dickson_one_one_eval_add_inv, dickson_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chebyshev_T_eq_dickson_one_one 📖	mathematical	—	Chebyshev.T Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat comp dickson instNatCast X	—	Nat.instAtLeastTwoHAddOfNat Chebyshev.T_eq_half_mul_C_comp_two_mul_X dickson_one_one_eq_chebyshev_C
chebyshev_U_eq_dickson_two_one 📖	mathematical	—	Chebyshev.U comp CommSemiring.toSemiring CommRing.toCommSemiring dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Polynomial instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat X	—	Nat.instAtLeastTwoHAddOfNat Chebyshev.S_comp_two_mul_X dickson_two_one_eq_chebyshev_S
dickson_add_two 📖	mathematical	—	dickson Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub CommRing.toRing instMul X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	dickson.eq_3
dickson_of_two_le 📖	mathematical	—	dickson Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub CommRing.toRing instMul X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	add_comm dickson_add_two
dickson_one 📖	mathematical	—	dickson X CommSemiring.toSemiring CommRing.toCommSemiring	—	—
dickson_one_one_charP 📖	mathematical	—	dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X	—	dvd_refl ZMod.cast_one' map_dickson dickson_one_one_zmod_p map_pow map_X
dickson_one_one_comp_comm 📖	mathematical	—	comp CommSemiring.toSemiring CommRing.toCommSemiring dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	dickson_one_one_mul mul_comm
dickson_one_one_eq_chebyshev_C 📖	mathematical	—	dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Chebyshev.C	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natCast Chebyshev.C_zero dickson_one Nat.cast_one Chebyshev.C_one dickson_add_two C_1 Nat.cast_add Nat.cast_two Chebyshev.C_add_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
dickson_one_one_eq_chebyshev_T 📖	mathematical	—	dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat comp Chebyshev.T DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast X	—	Nat.instAtLeastTwoHAddOfNat dickson_one_one_eq_chebyshev_C Chebyshev.C_eq_two_mul_T_comp_half_mul_X
dickson_one_one_eval_add_inv 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	eval CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd dickson Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat pow_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natCast eval_ofNat Mathlib.Meta.NormNum.isNat_add Nat.cast_one eval_X pow_one dickson_add_two eval_sub eval_mul eval_one pow_succ' mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass mul_comm one_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_pos
dickson_one_one_mul 📖	mathematical	—	dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing comp CommSemiring.toSemiring CommRing.toCommSemiring	—	eq_intCast RingHom.instRingHomClass Int.cast_one map_dickson map_injective Int.cast_injective Rat.instCharZero Nat.instAtLeastTwoHAddOfNat dickson_one_one_eq_chebyshev_T Nat.cast_mul Chebyshev.T_mul two_mul map_comp eval₂_congr comp_assoc mul_comp C_comp X_comp mul_assoc one_mul
dickson_one_one_zmod_p 📖	mathematical	—	dickson ZMod ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X	—	RingHom.charP_iff_charP FractionRing.instNontrivial nontrivial ZMod.nontrivial Nat.Prime.one_lt' ZMod.charP instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd ZMod.instIsDomain Infinite.of_injective infinite IsFractionRing.injective Localization.isLocalization map_injective dvd_refl RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial map_dickson map_pow map_X eq_of_infinite_eval_eq instIsDomain Set.Infinite.mono ZMod.cast_one' eval_pow eval_X dickson_one_one_eval_add_inv mul_inv_cancel₀ add_pow_char Set.infinite_univ_iff Set.eq_univ_of_forall inv_zero one_ne_zero NeZero.one Set.Finite.biUnion eval_zero sq eval_add eval_sub eval_mul MulZeroClass.mul_zero eval_C sub_self eval_one zero_add Set.ext mem_roots mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero sub_eq_zero add_mul Distrib.rightDistribClass inv_mul_cancel₀ eq_iff_eq_cancel_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Finset.finite_toSet
dickson_two 📖	mathematical	—	dickson Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sq
dickson_two_one_eq_chebyshev_S 📖	mathematical	—	dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Chebyshev.S	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_natCast Nat.cast_one Chebyshev.S_zero dickson_one Chebyshev.S_one dickson_add_two C_1 Nat.cast_add Nat.cast_two Chebyshev.S_add_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
dickson_two_one_eq_chebyshev_U 📖	mathematical	—	dickson AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing comp CommSemiring.toSemiring CommRing.toCommSemiring Chebyshev.U Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat X	—	Nat.instAtLeastTwoHAddOfNat dickson_two_one_eq_chebyshev_S Chebyshev.S_eq_U_comp_half_mul_X
dickson_two_zero 📖	mathematical	—	dickson MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X	—	Nat.instAtLeastTwoHAddOfNat pow_zero Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_natCast Nat.cast_one pow_one dickson_add_two C_0 MulZeroClass.zero_mul sub_zero pow_add mul_comm
dickson_zero 📖	mathematical	—	dickson Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub CommRing.toRing instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	—
map_dickson 📖	mathematical	—	map CommSemiring.toSemiring CommRing.toCommSemiring dickson DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Nat.instAtLeastTwoHAddOfNat map_sub map_natCast map_ofNat map_X dickson_add_two map_mul map_C

---

← Back to Index