Deriv

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

Statistics

Metric	Count
Definitions	0
Theorems `LogDeriv_exp`, `analyticAt_cos`, `analyticAt_sin`, `analyticOnNhd_cos`, `analyticOnNhd_sin`, `analyticOn_cos`, `analyticOn_sin`, `analyticWithinAt_cos`, `analyticWithinAt_sin`, `contDiff_cos`, `contDiff_sin`, `deriv_cos`, `deriv_cos'`, `deriv_sin`, `differentiableAt_cos`, `differentiableAt_sin`, `differentiable_cos`, `differentiable_iteratedDeriv_cos`, `differentiable_iteratedDeriv_sin`, `differentiable_sin`, `hasDerivAt_cos`, `hasDerivAt_sin`, `hasStrictDerivAt_cos`, `hasStrictDerivAt_sin`, `isEquivalent_sin`, `iteratedDeriv_add_one_cos`, `iteratedDeriv_add_one_sin`, `iteratedDeriv_even_cos`, `iteratedDeriv_even_sin`, `iteratedDeriv_odd_cos`, `iteratedDeriv_odd_sin`, `logDeriv_cos`, `logDeriv_exp`, `logDeriv_sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `ccos`, `cos`, `csin`, `sin`, `LogDeriv_exp`, `abs_iteratedDeriv_cos_le_one`, `abs_iteratedDeriv_sin_le_one`, `analyticAt_cos`, `analyticAt_sin`, `analyticOnNhd_cos`, `analyticOnNhd_sin`, `analyticOn_cos`, `analyticOn_sin`, `analyticWithinAt_cos`, `analyticWithinAt_sin`, `contDiff_cos`, `contDiff_sin`, `deriv_cos`, `deriv_cos'`, `deriv_sin`, `differentiableAt_cos`, `differentiableAt_sin`, `differentiable_cos`, `differentiable_iteratedDeriv_cos`, `differentiable_iteratedDeriv_sin`, `differentiable_sin`, `hasDerivAt_cos`, `hasDerivAt_sin`, `hasStrictDerivAt_cos`, `hasStrictDerivAt_sin`, `isEquivalent_sin`, `iteratedDerivWithin_cos_Icc`, `iteratedDerivWithin_cos_Ioo`, `iteratedDerivWithin_sin_Icc`, `iteratedDerivWithin_sin_Ioo`, `iteratedDeriv_add_one_cos`, `iteratedDeriv_add_one_sin`, `iteratedDeriv_even_cos`, `iteratedDeriv_even_sin`, `iteratedDeriv_odd_cos`, `iteratedDeriv_odd_sin`, `logDeriv_cos`, `logDeriv_exp`, `logDeriv_sin`, `derivWithin_ccos`, `derivWithin_cos`, `derivWithin_csin`, `derivWithin_sin`, `deriv_ccos`, `deriv_cos`, `deriv_csin`, `deriv_sin`, `fderivWithin_ccos`, `fderivWithin_cos`, `fderivWithin_csin`, `fderivWithin_sin`, `fderiv_ccos`, `fderiv_cos`, `fderiv_csin`, `fderiv_sin`	146
Total	146

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LogDeriv_exp` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `exp` `Pi.instOne` `instOne`	—	`logDeriv_exp`
`analyticAt_cos` 📖	mathematical	—	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiffAt.analyticAt` `ContDiff.contDiffAt` `contDiff_cos`
`analyticAt_sin` 📖	mathematical	—	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiffAt.analyticAt` `ContDiff.contDiffAt` `contDiff_sin`
`analyticOnNhd_cos` 📖	mathematical	—	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`analyticAt_cos`
`analyticOnNhd_sin` 📖	mathematical	—	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`analyticAt_sin`
`analyticOn_cos` 📖	mathematical	—	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiffOn.analyticOn` `ContDiff.contDiffOn` `contDiff_cos`
`analyticOn_sin` 📖	mathematical	—	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiffOn.analyticOn` `ContDiff.contDiffOn` `contDiff_sin`
`analyticWithinAt_cos` 📖	mathematical	—	`AnalyticWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiffWithinAt.analyticWithinAt` `ContDiff.contDiffWithinAt` `contDiff_cos`
`analyticWithinAt_sin` 📖	mathematical	—	`AnalyticWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiffWithinAt.analyticWithinAt` `ContDiff.contDiffWithinAt` `contDiff_sin`
`contDiff_cos` 📖	mathematical	—	`ContDiff` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiff.div_const` `ContDiff.add` `ContDiff.cexp` `ContDiff.mul` `contDiff_id` `contDiff_const` `contDiff_neg`
`contDiff_sin` 📖	mathematical	—	`ContDiff` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiff.div_const` `ContDiff.mul` `ContDiff.sub` `ContDiff.cexp` `contDiff_neg` `contDiff_const` `contDiff_id`
`deriv_cos` 📖	mathematical	—	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `cos` `instNeg` `sin`	—	`HasDerivAt.deriv` `hasDerivAt_cos`
`deriv_cos'` 📖	mathematical	—	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `cos` `instNeg` `sin`	—	`deriv_cos`
`deriv_sin` 📖	mathematical	—	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `sin` `cos`	—	`HasDerivAt.deriv` `hasDerivAt_sin`
`differentiableAt_cos` 📖	mathematical	—	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `cos`	—	`differentiable_cos`
`differentiableAt_sin` 📖	mathematical	—	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `sin`	—	`differentiable_sin`
`differentiable_cos` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `cos`	—	`HasDerivAt.differentiableAt` `hasDerivAt_cos`
`differentiable_iteratedDeriv_cos` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `iteratedDeriv` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`iteratedDeriv_zero` `iteratedDeriv_one` `deriv_cos'` `iteratedDeriv_add_one_cos` `iteratedDeriv_add_one_sin`
`differentiable_iteratedDeriv_sin` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `iteratedDeriv` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`iteratedDeriv_zero` `iteratedDeriv_one` `deriv_sin` `iteratedDeriv_add_one_sin` `iteratedDeriv_add_one_cos`
`differentiable_sin` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `sin`	—	`HasDerivAt.differentiableAt` `hasDerivAt_sin`
`hasDerivAt_cos` 📖	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` `cos` `instNeg` `sin`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_cos`
`hasDerivAt_sin` 📖	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` `sin` `cos`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_sin`
`hasStrictDerivAt_cos` 📖	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` `cos` `instNeg` `sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasStrictDerivAt.congr_simp` `div_eq_mul_inv` `neg_mul_eq_neg_mul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `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.one_mul` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `HasStrictDerivAt.mul_const` `HasStrictDerivAt.add` `HasStrictDerivAt.cexp` `hasStrictDerivAt_id` `HasStrictDerivAt.fun_neg`
`hasStrictDerivAt_sin` 📖	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` `sin` `cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasStrictDerivAt.congr_simp` `div_eq_mul_inv` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `sub_mul` `mul_assoc` `I_mul_I` `neg_one_mul` `neg_neg` `mul_one` `one_mul` `mul_neg_one` `sub_neg_eq_add` `add_comm` `HasStrictDerivAt.mul_const` `HasStrictDerivAt.sub` `HasStrictDerivAt.cexp` `HasStrictDerivAt.fun_neg` `hasStrictDerivAt_id`
`isEquivalent_sin` 📖	mathematical	—	`Asymptotics.IsEquivalent` `Complex` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `instZero` `sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `sin_zero` `sub_zero` `ContinuousLinearMap.toSpanSingleton.congr_simp` `cos_zero` `mul_one` `HasFDerivAtFilter.isLittleO` `hasDerivAt_sin`
`iteratedDeriv_add_one_cos` 📖	mathematical	—	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `Pi.instNeg` `instNeg` `sin`	—	`zero_add` `iteratedDeriv_one` `deriv_cos'` `iteratedDeriv_zero` `iteratedDeriv_succ` `deriv.neg'`
`iteratedDeriv_add_one_sin` 📖	mathematical	—	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `cos`	—	`zero_add` `iteratedDeriv_one` `deriv_sin` `iteratedDeriv_zero` `iteratedDeriv_succ`
`iteratedDeriv_even_cos` 📖	mathematical	—	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne`	—	`MulZeroClass.mul_zero` `iteratedDeriv_zero` `pow_zero` `one_mul` `mul_add` `Distrib.leftDistribClass` `mul_one` `iteratedDeriv_add_one_cos` `iteratedDeriv_add_one_sin` `pow_succ` `mul_neg` `neg_mul`
`iteratedDeriv_even_sin` 📖	mathematical	—	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne`	—	`MulZeroClass.mul_zero` `iteratedDeriv_zero` `pow_zero` `one_mul` `mul_add` `Distrib.leftDistribClass` `mul_one` `iteratedDeriv_add_one_sin` `iteratedDeriv_add_one_cos` `pow_succ` `mul_neg` `neg_mul`
`iteratedDeriv_odd_cos` 📖	mathematical	—	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne` `sin`	—	`iteratedDeriv_add_one_cos` `iteratedDeriv_even_sin` `pow_succ` `mul_neg` `mul_one` `neg_mul`
`iteratedDeriv_odd_sin` 📖	mathematical	—	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne` `cos`	—	`iteratedDeriv_add_one_sin` `iteratedDeriv_even_cos`
`logDeriv_cos` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `cos` `Pi.instNeg` `instNeg` `tan`	—	`logDeriv.eq_1` `deriv_cos'` `Pi.div_apply` `Pi.neg_apply` `tan.eq_1` `neg_div`
`logDeriv_exp` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `exp` `Pi.instOne` `instOne`	—	`logDeriv.eq_1` `deriv_exp` `Pi.div_apply` `exp_sub` `sub_self` `exp_zero` `Pi.one_apply`
`logDeriv_sin` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `sin` `cot`	—	`logDeriv.eq_1` `deriv_sin` `Pi.div_apply` `cot.eq_1`

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`ContDiff` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.cos`	—	`comp` `Complex.contDiff_cos`
`cos` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.cos`	—	`comp` `Real.contDiff_cos`
`csin` 📖	mathematical	`ContDiff` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.sin`	—	`comp` `Complex.contDiff_sin`
`sin` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.sin`	—	`comp` `Real.contDiff_sin`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`ContDiffAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.cos`	—	`comp` `ContDiff.contDiffAt` `Complex.contDiff_cos`
`cos` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.cos`	—	`comp` `ContDiff.contDiffAt` `Real.contDiff_cos`
`csin` 📖	mathematical	`ContDiffAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.sin`	—	`comp` `ContDiff.contDiffAt` `Complex.contDiff_sin`
`sin` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.sin`	—	`comp` `ContDiff.contDiffAt` `Real.contDiff_sin`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`ContDiffOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.cos`	—	`ContDiff.comp_contDiffOn` `Complex.contDiff_cos`
`cos` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.cos`	—	`ContDiff.comp_contDiffOn` `Real.contDiff_cos`
`csin` 📖	mathematical	`ContDiffOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.sin`	—	`ContDiff.comp_contDiffOn` `Complex.contDiff_sin`
`sin` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.sin`	—	`ContDiff.comp_contDiffOn` `Real.contDiff_sin`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`ContDiffWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.cos`	—	`ContDiffAt.comp_contDiffWithinAt` `ContDiff.contDiffAt` `Complex.contDiff_cos`
`cos` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.cos`	—	`ContDiffAt.comp_contDiffWithinAt` `ContDiff.contDiffAt` `Real.contDiff_cos`
`csin` 📖	mathematical	`ContDiffWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Complex.sin`	—	`ContDiffAt.comp_contDiffWithinAt` `ContDiff.contDiffAt` `Complex.contDiff_sin`
`sin` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real.sin`	—	`ContDiffAt.comp_contDiffWithinAt` `ContDiff.contDiffAt` `Real.contDiff_sin`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos`	—	`DifferentiableAt.ccos`
`cos` 📖	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.cos`	—	`DifferentiableAt.cos`
`csin` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin`	—	`DifferentiableAt.csin`
`sin` 📖	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.sin`	—	`DifferentiableAt.sin`

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos`	—	`HasFDerivAt.differentiableAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasFDerivAt.ccos` `hasFDerivAt`
`cos` 📖	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.cos`	—	`HasFDerivAt.differentiableAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasFDerivAt.cos` `hasFDerivAt`
`csin` 📖	mathematical	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin`	—	`HasFDerivAt.differentiableAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasFDerivAt.csin` `hasFDerivAt`
`sin` 📖	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.sin`	—	`HasFDerivAt.differentiableAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasFDerivAt.sin` `hasFDerivAt`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos`	—	`DifferentiableWithinAt.ccos`
`cos` 📖	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.cos`	—	`DifferentiableWithinAt.cos`
`csin` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin`	—	`DifferentiableWithinAt.csin`
`sin` 📖	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.sin`	—	`DifferentiableWithinAt.sin`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`DifferentiableWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos`	—	`HasFDerivWithinAt.differentiableWithinAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasFDerivWithinAt.ccos` `hasFDerivWithinAt`
`cos` 📖	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.cos`	—	`HasFDerivWithinAt.differentiableWithinAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasFDerivWithinAt.cos` `hasFDerivWithinAt`
`csin` 📖	mathematical	`DifferentiableWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin`	—	`HasFDerivWithinAt.differentiableWithinAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasFDerivWithinAt.csin` `hasFDerivWithinAt`
`sin` 📖	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.sin`	—	`HasFDerivWithinAt.differentiableWithinAt` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasFDerivWithinAt.sin` `hasFDerivWithinAt`

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.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`	`Complex.cos` `Complex.instMul` `Complex.instNeg` `Complex.sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `comp` `Complex.hasDerivAt_cos`
`cos` 📖	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.cos` `Real.instMul` `Real.instNeg` `Real.sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `comp` `Real.hasDerivAt_cos`
`csin` 📖	mathematical	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.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`	`Complex.sin` `Complex.instMul` `Complex.cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `comp` `Complex.hasDerivAt_sin`
`sin` 📖	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.sin` `Real.instMul` `Real.cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `comp` `Real.hasDerivAt_sin`

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`HasDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.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`	`Complex.cos` `Complex.instMul` `Complex.instNeg` `Complex.sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasDerivAt.comp_hasDerivWithinAt` `Complex.hasDerivAt_cos`
`cos` 📖	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.cos` `Real.instMul` `Real.instNeg` `Real.sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasDerivAt.comp_hasDerivWithinAt` `Real.hasDerivAt_cos`
`csin` 📖	mathematical	`HasDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.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`	`Complex.sin` `Complex.instMul` `Complex.cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasDerivAt.comp_hasDerivWithinAt` `Complex.hasDerivAt_sin`
`sin` 📖	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.sin` `Real.instMul` `Real.cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasDerivAt.comp_hasDerivWithinAt` `Real.hasDerivAt_sin`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`HasFDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Semiring.toModule` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instNeg` `Complex.sin`	—	`HasDerivAt.comp_hasFDerivAt` `Complex.hasDerivAt_cos`
`cos` 📖	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`	`Real.cos` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `Real.instNeg` `Real.sin`	—	`HasDerivAt.comp_hasFDerivAt` `Real.hasDerivAt_cos`
`csin` 📖	mathematical	`HasFDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Semiring.toModule` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.cos`	—	`HasDerivAt.comp_hasFDerivAt` `Complex.hasDerivAt_sin`
`sin` 📖	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`	`Real.sin` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `Real.cos`	—	`HasDerivAt.comp_hasFDerivAt` `Real.hasDerivAt_sin`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`HasFDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Semiring.toModule` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instNeg` `Complex.sin`	—	`HasDerivAt.comp_hasFDerivWithinAt` `Complex.hasDerivAt_cos`
`cos` 📖	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`	`Real.cos` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `Real.instNeg` `Real.sin`	—	`HasDerivAt.comp_hasFDerivWithinAt` `Real.hasDerivAt_cos`
`csin` 📖	mathematical	`HasFDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Semiring.toModule` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.cos`	—	`HasDerivAt.comp_hasFDerivWithinAt` `Complex.hasDerivAt_sin`
`sin` 📖	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`	`Real.sin` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `Real.cos`	—	`HasDerivAt.comp_hasFDerivWithinAt` `Real.hasDerivAt_sin`

HasStrictDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`HasStrictDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.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`	`Complex.cos` `Complex.instMul` `Complex.instNeg` `Complex.sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `comp` `Complex.hasStrictDerivAt_cos`
`cos` 📖	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.cos` `Real.instMul` `Real.instNeg` `Real.sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `comp` `Real.hasStrictDerivAt_cos`
`csin` 📖	mathematical	`HasStrictDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.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`	`Complex.sin` `Complex.instMul` `Complex.cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `comp` `Complex.hasStrictDerivAt_sin`
`sin` 📖	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.sin` `Real.instMul` `Real.cos`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `comp` `Real.hasStrictDerivAt_sin`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ccos` 📖	mathematical	`HasStrictFDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Semiring.toModule` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cos` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instNeg` `Complex.sin`	—	`HasStrictDerivAt.comp_hasStrictFDerivAt` `Complex.hasStrictDerivAt_cos`
`cos` 📖	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`	`Real.cos` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `Real.instNeg` `Real.sin`	—	`HasStrictDerivAt.comp_hasStrictFDerivAt` `Real.hasStrictDerivAt_cos`
`csin` 📖	mathematical	`HasStrictFDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Semiring.toModule` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.sin` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.cos`	—	`HasStrictDerivAt.comp_hasStrictFDerivAt` `Complex.hasStrictDerivAt_sin`
`sin` 📖	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`	`Real.sin` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `Real.cos`	—	`HasStrictDerivAt.comp_hasStrictFDerivAt` `Real.hasStrictDerivAt_sin`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LogDeriv_exp` 📖	mathematical	—	`logDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RCLike.toNormedAlgebra` `instRCLike` `exp` `Pi.instOne` `instOne`	—	`logDeriv_exp`
`abs_iteratedDeriv_cos_le_one` 📖	mathematical	—	`Real` `instLE` `abs` `lattice` `instAddGroup` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `instOne`	—	`iteratedDeriv_zero` `abs_cos_le_one` `iteratedDeriv_one` `deriv_cos'` `abs_neg` `abs_sin_le_one` `iteratedDeriv_add_one_cos` `iteratedDeriv_add_one_sin`
`abs_iteratedDeriv_sin_le_one` 📖	mathematical	—	`Real` `instLE` `abs` `lattice` `instAddGroup` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `instOne`	—	`iteratedDeriv_zero` `abs_sin_le_one` `iteratedDeriv_one` `deriv_sin` `abs_cos_le_one` `iteratedDeriv_add_one_sin` `iteratedDeriv_add_one_cos` `abs_neg`
`analyticAt_cos` 📖	mathematical	—	`AnalyticAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiffAt.analyticAt` `ContDiff.contDiffAt` `contDiff_cos`
`analyticAt_sin` 📖	mathematical	—	`AnalyticAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiffAt.analyticAt` `ContDiff.contDiffAt` `contDiff_sin`
`analyticOnNhd_cos` 📖	mathematical	—	`AnalyticOnNhd` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`analyticAt_cos`
`analyticOnNhd_sin` 📖	mathematical	—	`AnalyticOnNhd` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`analyticAt_sin`
`analyticOn_cos` 📖	mathematical	—	`AnalyticOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiffOn.analyticOn` `ContDiff.contDiffOn` `contDiff_cos`
`analyticOn_sin` 📖	mathematical	—	`AnalyticOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiffOn.analyticOn` `ContDiff.contDiffOn` `contDiff_sin`
`analyticWithinAt_cos` 📖	mathematical	—	`AnalyticWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiffWithinAt.analyticWithinAt` `ContDiff.contDiffWithinAt` `contDiff_cos`
`analyticWithinAt_sin` 📖	mathematical	—	`AnalyticWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiffWithinAt.analyticWithinAt` `ContDiff.contDiffWithinAt` `contDiff_sin`
`contDiff_cos` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos`	—	`ContDiff.real_of_complex` `Complex.contDiff_cos`
`contDiff_sin` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin`	—	`ContDiff.real_of_complex` `Complex.contDiff_sin`
`deriv_cos` 📖	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` `cos` `instNeg` `sin`	—	`HasDerivAt.deriv` `hasDerivAt_cos`
`deriv_cos'` 📖	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` `cos` `instNeg` `sin`	—	`deriv_cos`
`deriv_sin` 📖	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` `sin` `cos`	—	`HasDerivAt.deriv` `hasDerivAt_sin`
`differentiableAt_cos` 📖	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` `cos`	—	`differentiable_cos`
`differentiableAt_sin` 📖	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` `sin`	—	`differentiable_sin`
`differentiable_cos` 📖	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` `cos`	—	`HasDerivAt.differentiableAt` `hasDerivAt_cos`
`differentiable_iteratedDeriv_cos` 📖	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` `iteratedDeriv` `normedAddCommGroup` `NontriviallyNormedField.toNormedField` `cos`	—	`iteratedDeriv_zero` `iteratedDeriv_one` `deriv_cos'` `iteratedDeriv_add_one_cos` `iteratedDeriv_add_one_sin`
`differentiable_iteratedDeriv_sin` 📖	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` `iteratedDeriv` `normedAddCommGroup` `NontriviallyNormedField.toNormedField` `sin`	—	`iteratedDeriv_zero` `iteratedDeriv_one` `deriv_sin` `iteratedDeriv_add_one_sin` `iteratedDeriv_add_one_cos`
`differentiable_sin` 📖	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` `sin`	—	`HasDerivAt.differentiableAt` `hasDerivAt_sin`
`hasDerivAt_cos` 📖	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` `cos` `instNeg` `sin`	—	`HasDerivAt.real_of_complex` `Complex.hasDerivAt_cos`
`hasDerivAt_sin` 📖	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` `sin` `cos`	—	`HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt_sin`
`hasStrictDerivAt_cos` 📖	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` `cos` `instNeg` `sin`	—	`HasStrictDerivAt.real_of_complex` `Complex.hasStrictDerivAt_cos`
`hasStrictDerivAt_sin` 📖	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` `sin` `cos`	—	`HasStrictDerivAt.real_of_complex` `Complex.hasStrictDerivAt_sin`
`isEquivalent_sin` 📖	mathematical	—	`Asymptotics.IsEquivalent` `Real` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `sin`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `sin_zero` `sub_zero` `ContinuousLinearMap.toSpanSingleton.congr_simp` `cos_zero` `mul_one` `HasFDerivAtFilter.isLittleO` `hasDerivAt_sin`
`iteratedDerivWithin_cos_Icc` 📖	mathematical	`Real` `instLT` `Set` `Set.instMembership` `Set.Icc` `instPreorder`	`iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `iteratedDeriv`	—	`iteratedDerivWithin_eq_iteratedDeriv` `uniqueDiffOn_Icc` `ContDiff.contDiffAt` `contDiff_cos`
`iteratedDerivWithin_cos_Ioo` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `instPreorder`	`iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `iteratedDeriv`	—	`iteratedDerivWithin_eq_iteratedDeriv` `uniqueDiffOn_Ioo` `ContDiff.contDiffAt` `contDiff_cos`
`iteratedDerivWithin_sin_Icc` 📖	mathematical	`Real` `instLT` `Set` `Set.instMembership` `Set.Icc` `instPreorder`	`iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `iteratedDeriv`	—	`iteratedDerivWithin_eq_iteratedDeriv` `uniqueDiffOn_Icc` `ContDiff.contDiffAt` `contDiff_sin`
`iteratedDerivWithin_sin_Ioo` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `instPreorder`	`iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `iteratedDeriv`	—	`iteratedDerivWithin_eq_iteratedDeriv` `uniqueDiffOn_Ioo` `ContDiff.contDiffAt` `contDiff_sin`
`iteratedDeriv_add_one_cos` 📖	mathematical	—	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `Pi.instNeg` `instNeg` `sin`	—	`zero_add` `iteratedDeriv_one` `deriv_cos'` `iteratedDeriv_zero` `iteratedDeriv_succ` `deriv.neg'`
`iteratedDeriv_add_one_sin` 📖	mathematical	—	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `cos`	—	`zero_add` `iteratedDeriv_one` `deriv_sin` `iteratedDeriv_zero` `iteratedDeriv_succ`
`iteratedDeriv_even_cos` 📖	mathematical	—	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `instMonoid` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne`	—	`MulZeroClass.mul_zero` `iteratedDeriv_zero` `pow_zero` `one_mul` `mul_add` `Distrib.leftDistribClass` `mul_one` `iteratedDeriv_add_one_cos` `iteratedDeriv_add_one_sin` `pow_succ` `mul_neg` `neg_mul`
`iteratedDeriv_even_sin` 📖	mathematical	—	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `instMonoid` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne`	—	`MulZeroClass.mul_zero` `iteratedDeriv_zero` `pow_zero` `one_mul` `mul_add` `Distrib.leftDistribClass` `mul_one` `iteratedDeriv_add_one_sin` `iteratedDeriv_add_one_cos` `pow_succ` `mul_neg` `neg_mul`
`iteratedDeriv_odd_cos` 📖	mathematical	—	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `cos` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `instMonoid` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne` `sin`	—	`iteratedDeriv_add_one_cos` `iteratedDeriv_even_sin` `pow_succ` `mul_neg` `mul_one` `neg_mul`
`iteratedDeriv_odd_sin` 📖	mathematical	—	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `sin` `Pi.instMul` `instMul` `Pi.instPow` `Monoid.toNatPow` `instMonoid` `Pi.instNeg` `instNeg` `Pi.instOne` `instOne` `cos`	—	`iteratedDeriv_add_one_sin` `iteratedDeriv_even_cos`
`logDeriv_cos` 📖	mathematical	—	`logDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RCLike.toNormedAlgebra` `instRCLike` `cos` `Pi.instNeg` `instNeg` `tan`	—	`logDeriv.eq_1` `deriv_cos'` `Pi.div_apply` `Pi.neg_apply` `neg_div` `tan_eq_sin_div_cos`
`logDeriv_exp` 📖	mathematical	—	`logDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RCLike.toNormedAlgebra` `instRCLike` `exp` `Pi.instOne` `instOne`	—	`logDeriv.eq_1` `deriv_exp` `Pi.div_apply` `exp_sub` `sub_self` `exp_zero` `Pi.one_apply`
`logDeriv_sin` 📖	mathematical	—	`logDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RCLike.toNormedAlgebra` `instRCLike` `sin` `cot`	—	`logDeriv.eq_1` `deriv_sin` `Pi.div_apply` `cot_eq_cos_div_sin`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivWithin_ccos` 📖	mathematical	`DifferentiableWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `UniqueDiffWithinAt` `Complex.instSemiring`	`derivWithin` `Complex.cos` `Complex.instMul` `Complex.instNeg` `Complex.sin`	—	`HasDerivWithinAt.derivWithin` `HasDerivWithinAt.ccos` `DifferentiableWithinAt.hasDerivWithinAt`
`derivWithin_cos` 📖	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.cos` `Real.instMul` `Real.instNeg` `Real.sin`	—	`HasDerivWithinAt.derivWithin` `HasDerivWithinAt.cos` `DifferentiableWithinAt.hasDerivWithinAt`
`derivWithin_csin` 📖	mathematical	`DifferentiableWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `UniqueDiffWithinAt` `Complex.instSemiring`	`derivWithin` `Complex.sin` `Complex.instMul` `Complex.cos`	—	`HasDerivWithinAt.derivWithin` `HasDerivWithinAt.csin` `DifferentiableWithinAt.hasDerivWithinAt`
`derivWithin_sin` 📖	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.sin` `Real.instMul` `Real.cos`	—	`HasDerivWithinAt.derivWithin` `HasDerivWithinAt.sin` `DifferentiableWithinAt.hasDerivWithinAt`
`deriv_ccos` 📖	mathematical	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`deriv` `Complex.cos` `Complex.instMul` `Complex.instNeg` `Complex.sin`	—	`HasDerivAt.deriv` `HasDerivAt.ccos` `DifferentiableAt.hasDerivAt`
`deriv_cos` 📖	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.cos` `Real.instMul` `Real.instNeg` `Real.sin`	—	`HasDerivAt.deriv` `HasDerivAt.cos` `DifferentiableAt.hasDerivAt`
`deriv_csin` 📖	mathematical	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`deriv` `Complex.sin` `Complex.instMul` `Complex.cos`	—	`HasDerivAt.deriv` `HasDerivAt.csin` `DifferentiableAt.hasDerivAt`
`deriv_sin` 📖	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.sin` `Real.instMul` `Real.cos`	—	`HasDerivAt.deriv` `HasDerivAt.sin` `DifferentiableAt.hasDerivAt`
`fderivWithin_ccos` 📖	mathematical	`DifferentiableWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `UniqueDiffWithinAt` `Complex.instSemiring`	`fderivWithin` `Complex.cos` `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` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instNeg` `Complex.sin`	—	`HasFDerivWithinAt.fderivWithin` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMul.to_continuousSMul` `Complex.instT2Space` `HasFDerivWithinAt.ccos` `DifferentiableWithinAt.hasFDerivWithinAt`
`fderivWithin_cos` 📖	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.cos` `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` `Real.instNeg` `Real.sin`	—	`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.cos` `DifferentiableWithinAt.hasFDerivWithinAt`
`fderivWithin_csin` 📖	mathematical	`DifferentiableWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `UniqueDiffWithinAt` `Complex.instSemiring`	`fderivWithin` `Complex.sin` `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` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.cos`	—	`HasFDerivWithinAt.fderivWithin` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMul.to_continuousSMul` `Complex.instT2Space` `HasFDerivWithinAt.csin` `DifferentiableWithinAt.hasFDerivWithinAt`
`fderivWithin_sin` 📖	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.sin` `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` `Real.cos`	—	`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.sin` `DifferentiableWithinAt.hasFDerivWithinAt`
`fderiv_ccos` 📖	mathematical	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`fderiv` `Complex.cos` `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` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instNeg` `Complex.sin`	—	`HasFDerivAt.fderiv` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMul.to_continuousSMul` `Complex.instT2Space` `HasFDerivAt.ccos` `DifferentiableAt.hasFDerivAt`
`fderiv_cos` 📖	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.cos` `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` `Real.instNeg` `Real.sin`	—	`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.cos` `DifferentiableAt.hasFDerivAt`
`fderiv_csin` 📖	mathematical	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.addCommGroup` `Complex.instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`fderiv` `Complex.sin` `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` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.cos`	—	`HasFDerivAt.fderiv` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMul.to_continuousSMul` `Complex.instT2Space` `HasFDerivAt.csin` `DifferentiableAt.hasFDerivAt`
`fderiv_sin` 📖	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.sin` `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` `Real.cos`	—	`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.sin` `DifferentiableAt.hasFDerivAt`

---

← Back to Index