Documentation Verification Report

ComplexDeriv

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

Statistics

Metric	Count
Definitions	0
Theorems `contDiffAt_tan`, `continuousAt_tan`, `deriv_tan`, `differentiableAt_tan`, `hasDerivAt_tan`, `hasStrictDerivAt_tan`, `tendsto_norm_tan_atTop`, `tendsto_norm_tan_of_cos_eq_zero`	8
Total	8

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_tan` 📖	mathematical	—	`ContDiffAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `tan`	—	`continuousAt_tan` `ContDiffAt.continuousAt` `ContDiffAt.div` `ContDiff.contDiffAt` `contDiff_sin` `contDiff_cos`
`continuousAt_tan` 📖	mathematical	—	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `tan`	—	`not_tendsto_nhds_of_tendsto_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PerfectSpace.not_isolated` `instPerfectSpace` `tendsto_norm_tan_of_cos_eq_zero` `Filter.Tendsto.mono_left` `ContinuousAt.tendsto` `ContinuousAt.norm` `inf_le_left` `HasDerivAt.continuousAt` `hasDerivAt_tan`
`deriv_tan` 📖	mathematical	—	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `tan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `cos`	—	`differentiableAt_tan` `deriv_zero_of_not_differentiableAt` `sq` `MulZeroClass.mul_zero` `div_zero` `HasDerivAt.deriv` `hasDerivAt_tan`
`differentiableAt_tan` 📖	mathematical	—	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `tan`	—	`continuousAt_tan` `DifferentiableAt.continuousAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `HasDerivAt.differentiableAt` `hasDerivAt_tan`
`hasDerivAt_tan` 📖	mathematical	—	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `tan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `cos`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_tan`
`hasStrictDerivAt_tan` 📖	mathematical	—	`HasStrictDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `tan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Nat.cast_one` `sin_sq_add_cos_sq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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` `instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `HasStrictDerivAt.div` `hasStrictDerivAt_sin` `hasStrictDerivAt_cos`
`tendsto_norm_tan_atTop` 📖	mathematical	—	`Filter.Tendsto` `Complex` `Real` `Norm.norm` `instNorm` `tan` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `instAdd` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instIntCast` `instOne` `ofReal` `Real.pi` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `Real.instPreorder`	—	`tendsto_norm_tan_of_cos_eq_zero` `Nat.instAtLeastTwoHAddOfNat` `cos_eq_zero_iff`
`tendsto_norm_tan_of_cos_eq_zero` 📖	mathematical	`cos` `Complex` `instZero`	`Filter.Tendsto` `Real` `Norm.norm` `instNorm` `tan` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `Real.instPreorder`	—	`norm_div` `sq` `MulZeroClass.mul_zero` `add_zero` `NeZero.charZero_one` `instCharZero` `sin_sq_add_cos_sq` `HasDerivAt.tendsto_nhdsNE` `hasDerivAt_cos` `neg_ne_zero` `Filter.Tendsto.pos_mul_atTop` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `norm_pos_iff` `ContinuousWithinAt.norm` `Continuous.continuousWithinAt` `continuous_sin` `Filter.Tendsto.inv_tendsto_nhdsGT_zero` `Filter.Tendsto.comp` `tendsto_norm_nhdsNE_zero`

---

← Back to Index