ChebyshevGauss

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean

Statistics

Metric	Count
Definitions sumZeroes	1
Theorems integral_eq_sumZeroes, sumZeroes_T_of_not_dvd, sumZeroes_T_zero, sumZeroes_smul, sumZeroes_sum	5
Total	6

Polynomial.Chebyshev

Definitions

Name	Category	Theorems
sumZeroes 📖	CompOp	5 math math: integral_eq_sumZeroes, sumZeroes_T_of_not_dvd, sumZeroes_T_zero, sumZeroes_sum, sumZeroes_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_eq_sumZeroes 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree Real Real.semiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring WithBot.instCommSemiring Nat.instCommSemiring Nat.instPartialOrder Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instSemiring Nat.instLinearOrder Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instNonUnitalSemiring Nat.instStarRing Nat.instStarOrderedRing Nat.instNontrivial instOfNatAtLeastTwo WithBot.natCast Nat.instAtLeastTwoHAddOfNat	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Polynomial.eval Real.semiring sumZeroes	—	Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat Polynomial.mem_degreeLT Real.instIsDomain CharZero.NeZero.two RCLike.charZero_rclike Submodule.mem_span_image_finset_iff_exists_fun' Finset.coe_range Polynomial.Sequence.span_degreeLT Polynomial.eval_finset_sum Finset.sum_congr Polynomial.eval_smul IsScalarTower.right MeasureTheory.integral_finset_sum integrable_measureT Polynomial.continuousOn IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal sumZeroes_sum sumZeroes_smul MeasureTheory.integral_const_mul Nat.cast_zero integral_eval_T_real_measureT_zero sumZeroes_T_zero Nat.cast_one Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero zero_add mul_one Finset.mem_range integral_eval_T_real_measureT_of_ne_zero sumZeroes_T_of_not_dvd
sumZeroes_T_of_not_dvd 📖	mathematical	—	sumZeroes T Real Real.commRing Real.instZero	—	eq_or_ne CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike div_zero Finset.sum_congr MulZeroClass.mul_zero MulZeroClass.zero_mul Real.cos_zero T_eval_one Finset.sum_const zero_nsmul Nat.instAtLeastTwoHAddOfNat Complex.two_cos Int.cast_negOnePow Int.negOnePow_neg Int.coe_negOnePow Finset.sum_add_distrib Int.cast_neg neg_div neg_mul Complex.exp_neg add_mul Distrib.rightDistribClass mul_eq_zero_of_left Complex.exp_nat_mul inv_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Complex.ofReal_cos Complex.ofReal_mul Complex.ofReal_div Complex.ofReal_add Nat.cast_add Nat.cast_mul mul_eq_zero_iff_left NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass T_real_cos Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.instAtLeastTwo Finset.mul_sum
sumZeroes_T_zero 📖	mathematical	—	sumZeroes T Real Real.commRing Real.pi	—	Finset.sum_congr T_zero Polynomial.eval_one Finset.sum_const Finset.card_range nsmul_eq_mul mul_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Real.pi_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
sumZeroes_smul 📖	mathematical	—	sumZeroes Real Polynomial Real.semiring Algebra.toSMul Real.instCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id Real.instMul	—	Finset.sum_congr Polynomial.eval_smul IsScalarTower.right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
sumZeroes_sum 📖	mathematical	—	sumZeroes Finset.sum Polynomial Real Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Real.commRing Real.instAddCommMonoid	—	Finset.sum_congr Polynomial.eval_finset_sum Finset.sum_comm Finset.mul_sum

---

← Back to Index