Cotangent

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

Statistics

Metric	Count
Definitions cotTerm, sineTerm	2
Theorems cot_eq_exp_ratio, cot_pi_eq_exp_ratio, HasProdLocallyUniformlyOn_euler_sin_prod, HasProdUniformlyOn_sineTerm_prod_on_compact, Summable_cotTerm, cotTerm_identity, cot_pi_mul_contDiffWithinAt, cot_series_rep, cot_series_rep', differentiableOn_iteratedDerivWithin_cotTerm, eqOn_iteratedDerivWithin_cotTerm_integerComplement, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, eqOn_iteratedDeriv_cotTerm, euler_sineTerm_tprod, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, logDeriv_prod_sineTerm_eq_sum_cotTerm, logDeriv_sin_div_eq_cot, logDeriv_sineTerm_eq_cotTerm, multipliableUniformlyOn_euler_sin_prod_on_compact, multipliable_sineTerm, pi_mul_cot_pi_q_exp, sin_pi_mul_ne_zero, sineTerm_ne_zero, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, summable_cotTerm, tendsto_euler_sin_prod', tendsto_logDeriv_euler_cot_sub, tendsto_logDeriv_euler_sin_div	30
Total	32

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cot_eq_exp_ratio 📖	mathematical	—	cot Complex DivInvMonoid.toDiv instDivInvMonoid instAdd exp instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat I instOne instSub	—	Nat.instAtLeastTwoHAddOfNat cot.eq_1 sin.eq_1 cos.eq_1 mul_add Distrib.leftDistribClass exp_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Nat.cast_one Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.RingNF.mul_assoc_rev mul_assoc Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_add 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'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false instCharZero Nat.cast_zero Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.div_pf
cot_pi_eq_exp_ratio 📖	mathematical	—	cot Complex instMul ofReal Real.pi DivInvMonoid.toDiv instDivInvMonoid instAdd exp instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat I instOne instSub	—	Nat.instAtLeastTwoHAddOfNat cot_eq_exp_ratio Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf' 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 Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt 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.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.div_pf mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg

(root)

Definitions

Name	Category	Theorems
cotTerm 📖	CompOp	11 math math: differentiableOn_iteratedDerivWithin_cotTerm, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, Summable_cotTerm, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, eqOn_iteratedDeriv_cotTerm, tendsto_logDeriv_euler_cot_sub, cotTerm_identity, logDeriv_prod_sineTerm_eq_sum_cotTerm, summable_cotTerm, eqOn_iteratedDerivWithin_cotTerm_integerComplement, logDeriv_sineTerm_eq_cotTerm
sineTerm 📖	CompOp	9 math math: HasProdUniformlyOn_sineTerm_prod_on_compact, tendsto_logDeriv_euler_sin_div, HasProdLocallyUniformlyOn_euler_sin_prod, multipliable_sineTerm, euler_sineTerm_tprod, logDeriv_prod_sineTerm_eq_sum_cotTerm, tendsto_euler_sin_prod', multipliableUniformlyOn_euler_sin_prod_on_compact, logDeriv_sineTerm_eq_cotTerm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HasProdLocallyUniformlyOn_euler_sin_prod 📖	mathematical	—	HasProdLocallyUniformlyOn Complex CommRing.toCommMonoid Complex.commRing Complex.instAdd Complex.instOne sineTerm DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul Complex.ofReal Real.pi Complex.integerComplement PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField UniformSpace.toTopologicalSpace	—	hasProdLocallyUniformlyOn_of_forall_compact Complex.isOpen_compl_range_intCast locallyCompact_of_proper Complex.instProperSpace HasProdUniformlyOn_sineTerm_prod_on_compact
HasProdUniformlyOn_sineTerm_prod_on_compact 📖	mathematical	Set Complex Set.instHasSubset Complex.integerComplement IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	HasProdUniformlyOn CommRing.toCommMonoid Complex.commRing Complex.instAdd Complex.instOne sineTerm DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul Complex.ofReal Real.pi	—	HasProdUniformlyOn.congr_right MultipliableUniformlyOn.hasProdUniformlyOn multipliableUniformlyOn_euler_sin_prod_on_compact euler_sineTerm_tprod
Summable_cotTerm 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup cotTerm SummationFilter.unconditional	—	summable_cotTerm
cotTerm_identity 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	cotTerm Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instAdd Complex.instSub	—	Nat.instAtLeastTwoHAddOfNat one_div_add_one_div sub_eq_add_neg neg_add_rev Int.cast_add Int.cast_neg Int.cast_one Int.cast_natCast Complex.integerComplement_add_ne_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_mul 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_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add 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.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.instAtLeastTwo
cot_pi_mul_contDiffWithinAt 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	ContDiffWithinAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace WithTop.some ENat Complex.cot Complex.instMul Complex.ofReal Real.pi UpperHalfPlane.upperHalfPlaneSet	—	ContDiffWithinAt.div ContDiffWithinAt.div_const ContDiffWithinAt.add ContDiffWithinAt.cexp ContDiffWithinAt.mul contDiffWithinAt_const contDiffWithinAt_fun_id ContDiffWithinAt.neg ContDiffWithinAt.sub sin_pi_mul_ne_zero
cot_series_rep 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	Complex.instMul Complex.ofReal Real.pi Complex.cot Complex.instAdd DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne tsum PNat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instSub Complex.instNatCast PNat.val SummationFilter.unconditional	—	tsum_pnat_eq_tsum_succ cot_series_rep' one_div Nat.cast_add Nat.cast_one Mathlib.Tactic.Ring.of_eq 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.add_congr Mathlib.Tactic.Ring.inv_congr 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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt 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
cot_series_rep' 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	Complex.instSub Complex.instMul Complex.ofReal Real.pi Complex.cot DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instAdd Complex.instNatCast SummationFilter.unconditional	—	HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional Summable.hasSum_iff_tendsto_nat summable_cotTerm tendsto_logDeriv_euler_cot_sub
differentiableOn_iteratedDerivWithin_cotTerm 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField iteratedDerivWithin Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace cotTerm UpperHalfPlane.upperHalfPlaneSet	—	DifferentiableOn.const_mul DifferentiableOn.add DifferentiableOn.zpow DifferentiableOn.add_const differentiableOn_id neg_add_rev Int.cast_add Int.cast_neg Int.cast_one Int.cast_natCast UpperHalfPlane.ne_intCast DifferentiableOn.sub_const DifferentiableOn.congr eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet
eqOn_iteratedDerivWithin_cotTerm_integerComplement 📖	mathematical	—	Set.EqOn Complex iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace cotTerm Complex.integerComplement Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.instNatCast Nat.factorial Complex.instAdd DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instSub	—	Set.EqOn.trans iteratedDerivWithin_of_isOpen Complex.isOpen_compl_range_intCast eqOn_iteratedDeriv_cotTerm
eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet 📖	mathematical	—	Set.EqOn Complex iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace cotTerm UpperHalfPlane.upperHalfPlaneSet Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.instNatCast Nat.factorial Complex.instAdd DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instSub	—	Set.EqOn.trans iteratedDerivWithin_congr_right_of_isOpen UpperHalfPlane.isOpen_upperHalfPlaneSet Complex.isOpen_compl_range_intCast Complex.upperHalfPlane_inter_integerComplement eqOn_iteratedDerivWithin_cotTerm_integerComplement UpperHalfPlane.coe_mem_integerComplement
eqOn_iteratedDeriv_cotTerm 📖	mathematical	—	Set.EqOn Complex iteratedDeriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace cotTerm Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.instNatCast Nat.factorial Complex.instAdd DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instSub Complex.integerComplement	—	Pi.add_def iteratedDeriv_add sub_eq_add_neg neg_add_rev one_div Int.cast_add Int.cast_neg Int.cast_one Int.cast_natCast ContDiffOn.contDiffAt IsOpen.mem_nhds Complex.isOpen_compl_range_intCast iter_deriv_inv_linear_sub iter_deriv_inv_linear iteratedDeriv_eq_iterate one_mul one_pow mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add 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.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
euler_sineTerm_tprod 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	tprod CommRing.toCommMonoid Complex.commRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instAdd Complex.instOne sineTerm SummationFilter.unconditional DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul Complex.ofReal Real.pi	—	Multipliable.hasProd_iff Complex.instT2Space SummationFilter.instNeBotUnconditional multipliable_sineTerm Multipliable.hasProd_iff_tendsto_nat tendsto_euler_sin_prod' Complex.integerComplement.ne_zero
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow 📖	mathematical	Complex Set Set.instMembership UpperHalfPlane.upperHalfPlaneSet	iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul Complex.ofReal Real.pi Complex.cot Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.instNatCast Nat.factorial tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instIntCast SummationFilter.unconditional	—	Nat.cast_one zpow_neg_coe_of_pos one_div iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow 📖	mathematical	Complex Set Set.instMembership UpperHalfPlane.upperHalfPlaneSet	iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul Complex.ofReal Real.pi Complex.cot Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.instNatCast Nat.factorial tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instAdd Complex.instIntCast SummationFilter.unconditional	—	AddRightCancelSemigroup.toIsRightCancelAdd add_comm iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add 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.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.neg_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf
iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum 📖	mathematical	Complex Set Set.instMembership UpperHalfPlane.upperHalfPlaneSet	iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instSub Complex.instMul Complex.ofReal Real.pi Complex.cot DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instAdd Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNatCast Nat.factorial DivInvMonoid.toZPow tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instIntCast SummationFilter.unconditional	—	one_div neg_mul neg_add_cancel_left iteratedDerivWithin_congr cot_series_rep' UpperHalfPlane.coe_mem_integerComplement
logDeriv_prod_sineTerm_eq_sum_cotTerm 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	logDeriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedAlgebra.id NontriviallyNormedField.toNormedField Finset.prod CommRing.toCommMonoid Complex.commRing Finset.range Complex.instAdd Complex.instOne sineTerm Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup cotTerm	—	logDeriv_prod sineTerm_ne_zero DifferentiableAt.const_add DifferentiableAt.div_const DifferentiableAt.fun_neg DifferentiableAt.fun_pow differentiableAt_id Finset.sum_congr logDeriv_sineTerm_eq_cotTerm
logDeriv_sin_div_eq_cot 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	logDeriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedAlgebra.id NontriviallyNormedField.toNormedField DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul Complex.ofReal Real.pi Complex.instSub Complex.cot Complex.instOne	—	logDeriv_div sin_pi_mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.pi_ne_zero Complex.integerComplement.ne_zero DifferentiableAt.comp Complex.differentiableAt_sin DifferentiableAt.const_mul differentiableAt_id logDeriv_comp Complex.logDeriv_sin deriv_const_mul deriv_id'' logDeriv_const_mul logDeriv_id' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.mul_pf_right Mathlib.Tactic.Ring.div_congr 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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw 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.add_pf_zero_add
logDeriv_sineTerm_eq_cotTerm 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	logDeriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedAlgebra.id NontriviallyNormedField.toNormedField Complex.instAdd Complex.instOne sineTerm cotTerm	—	Complex.integerComplement_add_ne_zero sub_eq_add_neg neg_add_rev Int.cast_add Int.cast_neg Int.cast_one Int.cast_natCast Complex.integerComplement_pow_two_ne_pow_two sub_ne_zero Nat.instAtLeastTwoHAddOfNat deriv_const_add' deriv_div_const deriv.fun_neg' deriv_fun_pow deriv_id'' Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_add 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'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Complex.instCharZero Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval mul_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Meta.NormNum.isNat_natSub Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add 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 Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Meta.NormNum.isNat_mul
multipliableUniformlyOn_euler_sin_prod_on_compact 📖	mathematical	IsCompact Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	MultipliableUniformlyOn CommRing.toCommMonoid Complex.commRing Complex.instAdd Complex.instOne sineTerm	—	Summable.multipliableUniformlyOn_nat_one_add NormedDivisionRing.to_normOneClass Complex.instCompleteSpace Filter.univ_mem' Continuous.comp_continuousOn' Continuous.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_id' ContinuousOn.neg IsTopologicalRing.toContinuousNeg ContinuousOn.pow continuousOn_id'
multipliable_sineTerm 📖	mathematical	—	Multipliable Complex CommRing.toCommMonoid Complex.commRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instAdd Complex.instOne sineTerm SummationFilter.unconditional	—	multipliable_one_add_of_summable NormedDivisionRing.to_normOneClass Complex.instCompleteSpace summable_pow_div_add Complex.norm_div norm_neg norm_pow NormedDivisionRing.toNormMulClass Nat.cast_one
pi_mul_cot_pi_q_exp 📖	mathematical	—	Complex Complex.instMul Complex.ofReal Real.pi Complex.cot UpperHalfPlane.coe Complex.instSub Complex.I instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.exp SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat div_mul_eq_div_mul_one_div Complex.div_I one_div neg_mul mul_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_congr 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.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.atom_pf' Complex.cot_pi_eq_exp_ratio tsum_geometric_of_norm_lt_one UpperHalfPlane.norm_exp_two_pi_I_lt_one add_comm geom_series_mul_one_add instHasSummableGeomSeries Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat
sin_pi_mul_ne_zero 📖	—	Complex Set Set.instMembership Complex.integerComplement	—	—	Complex.sin_ne_zero_iff mul_comm mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Complex.ofReal_ne_zero Real.pi_ne_zero Complex.instCharZero
sineTerm_ne_zero 📖	—	Complex Set Set.instMembership Complex.integerComplement	—	—	add_eq_zero_iff_eq_neg neg_div' eq_div_iff isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Nat.cast_add_one_ne_zero Complex.instCharZero Complex.integerComplement_pow_two_ne_pow_two one_mul neg_neg Int.cast_add Int.cast_natCast Int.cast_one
summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm 📖	mathematical	—	SummableLocallyUniformlyOn Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace cotTerm UpperHalfPlane.upperHalfPlaneSet	—	SummableLocallyUniformlyOn_of_locally_bounded Complex.instCompleteSpace locallyCompact_of_proper Complex.instProperSpace UpperHalfPlane.isOpen_upperHalfPlaneSet CanLift.prf Set.canLift UpperHalfPlane.canLift UpperHalfPlane.subset_verticalStrip_of_isCompact Topology.IsEmbedding.isCompact_iff UpperHalfPlane.isEmbedding_coe Set.image_mono
summable_cotTerm 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup cotTerm SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat cotTerm_identity Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Summable.congr EisensteinSeries.summable_linear_sub_mul_linear_add Int.cast_one mul_comm mul_one mul_inv_rev Summable.comp_injective SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace CharZero.cast_injective Int.instCharZero one_div Nat.cast_add Nat.cast_one summable_nat_add_iff SeminormedAddCommGroup.toIsTopologicalAddGroup
tendsto_euler_sin_prod' 📖	mathematical	—	Filter.Tendsto Complex Finset.prod CommRing.toCommMonoid Complex.commRing Finset.range Complex.instAdd Complex.instOne sineTerm Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul Complex.ofReal Real.pi	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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.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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Filter.Tendsto.congr Filter.Tendsto.mul_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.tendsto_euler_sin_prod 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.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Finset.prod_congr Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero neg_div mul_neg one_ne_zero NeZero.one GroupWithZero.toNontrivial
tendsto_logDeriv_euler_cot_sub 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	Filter.Tendsto Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.range cotTerm Filter.atTop Nat.instPreorder nhds Complex.instSub Complex.instMul Complex.ofReal Real.pi Complex.cot DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne	—	logDeriv_sin_div_eq_cot logDeriv_prod_sineTerm_eq_sum_cotTerm tendsto_logDeriv_euler_sin_div
tendsto_logDeriv_euler_sin_div 📖	mathematical	Complex Set Set.instMembership Complex.integerComplement	Filter.Tendsto logDeriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedAlgebra.id NontriviallyNormedField.toNormedField Finset.prod CommRing.toCommMonoid Complex.commRing Finset.range Complex.instAdd Complex.instOne sineTerm Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul Complex.ofReal Real.pi	—	Complex.logDeriv_tendsto Complex.isOpen_compl_range_intCast HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange HasProdLocallyUniformlyOn_euler_sin_prod Filter.univ_mem' DifferentiableOn.fun_finset_prod DifferentiableOn.const_add DifferentiableOn.div_const DifferentiableOn.fun_neg DifferentiableOn.fun_pow differentiableOn_id NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass sin_pi_mul_ne_zero Real.pi_ne_zero Complex.integerComplement.ne_zero

---

← Back to Index