Basic

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

Statistics

Metric	Count
Definitions	0
Theorems C_two_mul_complex_cos, C_two_mul_complex_cosh, C_two_mul_real_cos, C_two_mul_real_cosh, S_two_mul_complex_cos, S_two_mul_complex_cosh, S_two_mul_real_cos, S_two_mul_real_cosh, T_complex_cos, T_complex_cosh, T_real_cos, T_real_cosh, U_complex_cos, U_complex_cosh, U_real_cos, U_real_cosh, complex_ofReal_eval_C, complex_ofReal_eval_S, complex_ofReal_eval_T, complex_ofReal_eval_U	20
Total	20

Polynomial.Chebyshev

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_two_mul_complex_cos 📖	mathematical	—	Polynomial.eval Complex CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.cos C Complex.instIntCast	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero C_eq_two_mul_T_comp_half_mul_X invOf_eq_inv Polynomial.eval_mul Polynomial.eval_ofNat Polynomial.eval_comp Polynomial.eval_C Polynomial.eval_X inv_mul_cancel_left₀ T_complex_cos
C_two_mul_complex_cosh 📖	mathematical	—	Polynomial.eval Complex CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.cosh C Complex.instIntCast	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero C_eq_two_mul_T_comp_half_mul_X invOf_eq_inv Polynomial.eval_mul Polynomial.eval_ofNat Polynomial.eval_comp Polynomial.eval_C Polynomial.eval_X inv_mul_cancel_left₀ T_complex_cosh
C_two_mul_real_cos 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cos C Real.instIntCast	—	C_two_mul_complex_cos
C_two_mul_real_cosh 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cosh C Real.instIntCast	—	C_two_mul_complex_cosh
S_two_mul_complex_cos 📖	mathematical	—	Complex Complex.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.cos S Complex.sin Complex.instAdd Complex.instIntCast Complex.instOne	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero S_eq_U_comp_half_mul_X invOf_eq_inv Polynomial.eval_comp Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_X inv_mul_cancel_left₀ U_complex_cos
S_two_mul_complex_cosh 📖	mathematical	—	Complex Complex.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.cosh S Complex.sinh Complex.instAdd Complex.instIntCast Complex.instOne	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero S_eq_U_comp_half_mul_X invOf_eq_inv Polynomial.eval_comp Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_X inv_mul_cancel_left₀ U_complex_cosh
S_two_mul_real_cos 📖	mathematical	—	Real Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cos S Real.sin Real.instAdd Real.instIntCast Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Int.cast_one Int.cast_add Complex.ofReal_add S_two_mul_complex_cos
S_two_mul_real_cosh 📖	mathematical	—	Real Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cosh S Real.sinh Real.instAdd Real.instIntCast Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one Int.cast_one Int.cast_add Complex.ofReal_add S_two_mul_complex_cosh
T_complex_cos 📖	mathematical	—	Polynomial.eval Complex CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing Complex.cos T Complex.instMul Complex.instIntCast	—	induct T_zero Polynomial.eval_one Int.cast_zero MulZeroClass.zero_mul Complex.cos_zero T_one Polynomial.eval_X Int.cast_one one_mul Nat.instAtLeastTwoHAddOfNat T_add_two Polynomial.eval_sub Polynomial.eval_mul Polynomial.eval_ofNat Complex.cos_add_cos Int.cast_add Int.cast_natCast Int.cast_ofNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add T_sub_one Int.cast_neg Int.cast_sub Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat
T_complex_cosh 📖	mathematical	—	Polynomial.eval Complex CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing Complex.cosh T Complex.instMul Complex.instIntCast	—	Complex.cos_mul_I T_complex_cos mul_assoc
T_real_cos 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.cos T Real.instMul Real.instIntCast	—	T_complex_cos
T_real_cosh 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.cosh T Real.instMul Real.instIntCast	—	T_complex_cosh
U_complex_cos 📖	mathematical	—	Complex Complex.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing Complex.cos U Complex.sin Complex.instAdd Complex.instIntCast Complex.instOne	—	induct U_zero Polynomial.eval_one one_mul Int.cast_zero zero_add Nat.instAtLeastTwoHAddOfNat U_one Polynomial.eval_mul Polynomial.eval_ofNat Polynomial.eval_X Int.cast_one one_add_one_eq_two Complex.sin_two_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left U_add_two mul_assoc Polynomial.eval_sub sub_mul Complex.sin_add_sin Int.cast_add Int.cast_natCast Int.cast_ofNat Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_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.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.sub_congr 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add U_sub_one Int.cast_neg Int.cast_sub Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat
U_complex_cosh 📖	mathematical	—	Complex Complex.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing Complex.cosh U Complex.sinh Complex.instAdd Complex.instIntCast Complex.instOne	—	Complex.cos_mul_I Complex.sin_mul_I mul_neg mul_assoc Complex.I_mul_I mul_one neg_neg U_complex_cos
U_real_cos 📖	mathematical	—	Real Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.cos U Real.sin Real.instAdd Real.instIntCast Real.instOne	—	Nat.cast_one Int.cast_one Int.cast_add Complex.ofReal_add U_complex_cos
U_real_cosh 📖	mathematical	—	Real Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.cosh U Real.sinh Real.instAdd Real.instIntCast Real.instOne	—	Nat.cast_one Int.cast_one Int.cast_add Complex.ofReal_add U_complex_cosh
complex_ofReal_eval_C 📖	mathematical	—	Complex.ofReal Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing C Complex Complex.commRing	—	algebraMap_eval_C
complex_ofReal_eval_S 📖	mathematical	—	Complex.ofReal Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing S Complex Complex.commRing	—	algebraMap_eval_S
complex_ofReal_eval_T 📖	mathematical	—	Complex.ofReal Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Complex Complex.commRing	—	algebraMap_eval_T
complex_ofReal_eval_U 📖	mathematical	—	Complex.ofReal Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing U Complex Complex.commRing	—	algebraMap_eval_U

---

← Back to Index