Documentation Verification Report

ArctanDeriv

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

Statistics

Metric	Count
Definitions	0
Theorems `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `arctan`, `contDiffAt_tan`, `contDiff_arctan`, `continuousAt_tan`, `deriv_arctan`, `deriv_tan`, `differentiableAt_arctan`, `differentiableAt_tan`, `differentiableAt_tan_of_mem_Ioo`, `differentiable_arctan`, `hasDerivAt_arctan`, `hasDerivAt_arctan'`, `hasDerivAt_tan`, `hasDerivAt_tan_of_mem_Ioo`, `hasStrictDerivAt_arctan`, `hasStrictDerivAt_tan`, `tendsto_abs_tan_atTop`, `tendsto_abs_tan_of_cos_eq_zero`, `derivWithin_arctan`, `deriv_arctan`, `fderivWithin_arctan`, `fderiv_arctan`	35
Total	35

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat`	`Real.arctan`	—	`comp` `Real.contDiff_arctan`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat`	`Real.arctan`	—	`comp` `ContDiff.contDiffAt` `Real.contDiff_arctan`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat`	`Real.arctan`	—	`ContDiff.comp_contDiffOn` `Real.contDiff_arctan`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat`	`Real.arctan`	—	`ContDiff.comp_contDiffWithinAt` `Real.contDiff_arctan`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace`	`Real.arctan`	—	`DifferentiableAt.arctan`

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace`	`Real.arctan`	—	`HasFDerivAt.differentiableAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasFDerivAt.arctan` `hasFDerivAt`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`DifferentiableOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace`	`Real.arctan`	—	`DifferentiableWithinAt.arctan`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace`	`Real.arctan`	—	`HasFDerivWithinAt.differentiableWithinAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasFDerivWithinAt.arctan` `hasFDerivWithinAt`

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`Real.arctan` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `comp` `Real.hasDerivAt_arctan`

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`HasDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`Real.arctan` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasDerivAt.comp_hasDerivWithinAt` `Real.hasDerivAt_arctan`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace`	`NormedAddCommGroup.toAddCommGroup` `Real.arctan` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasDerivAt.comp_hasFDerivAt` `Real.hasDerivAt_arctan`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace`	`NormedAddCommGroup.toAddCommGroup` `Real.arctan` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasDerivAt.comp_hasFDerivWithinAt` `Real.hasDerivAt_arctan`

HasStrictDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`HasStrictDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`Real.arctan` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `comp` `Real.hasStrictDerivAt_arctan`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arctan` 📖	mathematical	`HasStrictFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `Semiring.toModule` `Real.semiring` `Real.pseudoMetricSpace`	`NormedAddCommGroup.toAddCommGroup` `Real.arctan` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasStrictDerivAt.comp_hasStrictFDerivAt` `Real.hasStrictDerivAt_arctan`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_tan` 📖	mathematical	—	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `tan`	—	`continuousAt_tan` `ContDiffAt.continuousAt` `ContDiffAt.real_of_complex` `Complex.contDiffAt_tan` `Nat.cast_zero`
`contDiff_arctan` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `arctan`	—	`contDiff_iff_contDiffAt` `LT.lt.ne'` `cos_arctan_pos` `OpenPartialHomeomorph.contDiffAt_symm_deriv` `instCompleteSpace` `one_div` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `hasDerivAt_tan` `contDiffAt_tan`
`continuousAt_tan` 📖	mathematical	—	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `tan`	—	`not_tendsto_nhds_of_tendsto_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `PerfectSpace.not_isolated` `instPerfectSpace` `tendsto_abs_tan_of_cos_eq_zero` `Filter.Tendsto.mono_left` `ContinuousAt.tendsto` `ContinuousAt.norm` `inf_le_left` `HasDerivAt.continuousAt` `hasDerivAt_tan`
`deriv_arctan` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `arctan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instAdd` `Monoid.toNatPow` `instMonoid`	—	`HasDerivAt.deriv` `hasDerivAt_arctan`
`deriv_tan` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `tan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `instMonoid` `cos`	—	`differentiableAt_tan` `deriv_zero_of_not_differentiableAt` `sq` `MulZeroClass.mul_zero` `div_zero` `HasDerivAt.deriv` `hasDerivAt_tan`
`differentiableAt_arctan` 📖	mathematical	—	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `arctan`	—	`HasDerivAt.differentiableAt` `hasDerivAt_arctan`
`differentiableAt_tan` 📖	mathematical	—	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `tan`	—	`continuousAt_tan` `DifferentiableAt.continuousAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `HasDerivAt.differentiableAt` `hasDerivAt_tan`
`differentiableAt_tan_of_mem_Ioo` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `instPreorder` `instNeg` `DivInvMonoid.toDiv` `instDivInvMonoid` `pi` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `tan`	—	`Nat.instAtLeastTwoHAddOfNat` `HasDerivAt.differentiableAt` `hasDerivAt_tan_of_mem_Ioo`
`differentiable_arctan` 📖	mathematical	—	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `arctan`	—	`differentiableAt_arctan`
`hasDerivAt_arctan` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `arctan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instAdd` `Monoid.toNatPow` `instMonoid`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_arctan`
`hasDerivAt_arctan'` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `arctan` `instInv` `instAdd` `instOne` `Monoid.toNatPow` `instMonoid`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasDerivAt_arctan` `one_div`
`hasDerivAt_tan` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `tan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `instMonoid` `cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasDerivAt.congr_simp` `Nat.cast_one` `HasDerivAt.real_of_complex` `Complex.hasDerivAt_tan` `Nat.cast_zero`
`hasDerivAt_tan_of_mem_Ioo` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `instPreorder` `instNeg` `DivInvMonoid.toDiv` `instDivInvMonoid` `pi` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `tan` `instOne` `Monoid.toNatPow` `instMonoid` `cos`	—	`Nat.instAtLeastTwoHAddOfNat` `hasDerivAt_tan` `LT.lt.ne'` `cos_pos_of_mem_Ioo`
`hasStrictDerivAt_arctan` 📖	mathematical	—	`HasStrictDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `arctan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instAdd` `Monoid.toNatPow` `instMonoid`	—	`LT.lt.ne'` `cos_arctan_pos` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasStrictDerivAt.congr_simp` `one_div` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `cos_sq_arctan` `div_inv_eq_mul` `one_mul` `OpenPartialHomeomorph.hasStrictDerivAt_symm` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `hasStrictDerivAt_tan`
`hasStrictDerivAt_tan` 📖	mathematical	—	`HasStrictDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `tan` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `instMonoid` `cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasStrictDerivAt.congr_simp` `Nat.cast_one` `HasStrictDerivAt.real_of_complex` `Complex.hasStrictDerivAt_tan` `Nat.cast_zero`
`tendsto_abs_tan_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `abs` `lattice` `instAddGroup` `tan` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `instAdd` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instIntCast` `instOne` `pi` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `instPreorder`	—	`tendsto_abs_tan_of_cos_eq_zero` `Nat.instAtLeastTwoHAddOfNat` `cos_eq_zero_iff`
`tendsto_abs_tan_of_cos_eq_zero` 📖	mathematical	`cos` `Real` `instZero`	`Filter.Tendsto` `abs` `lattice` `instAddGroup` `tan` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `instPreorder`	—	`Nat.cast_zero` `Complex.ofReal_tan` `Filter.Tendsto.comp` `Complex.tendsto_norm_tan_of_cos_eq_zero` `Filter.Tendsto.inf` `Continuous.continuousAt` `Complex.continuous_ofReal` `Filter.tendsto_principal_principal`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivWithin_arctan` 📖	mathematical	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `UniqueDiffWithinAt` `Real.semiring`	`derivWithin` `Real.arctan` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasDerivWithinAt.derivWithin` `HasDerivWithinAt.arctan` `DifferentiableWithinAt.hasDerivWithinAt`
`deriv_arctan` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`deriv` `Real.arctan` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasDerivAt.deriv` `HasDerivAt.arctan` `DifferentiableAt.hasDerivAt`
`fderivWithin_arctan` 📖	mathematical	`DifferentiableWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace` `UniqueDiffWithinAt` `Real.semiring`	`fderivWithin` `Real.arctan` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasFDerivWithinAt.fderivWithin` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMul.to_continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivWithinAt.arctan` `DifferentiableWithinAt.hasFDerivWithinAt`
`fderiv_arctan` 📖	mathematical	`DifferentiableAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace`	`fderiv` `Real.arctan` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid`	—	`HasFDerivAt.fderiv` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMul.to_continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivAt.arctan` `DifferentiableAt.hasFDerivAt`

---

← Back to Index