CauchyIntegral

📁 Source: Mathlib/Analysis/Complex/CauchyIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems `analyticAt_iff_eventually_differentiableAt`, `analyticOnNhd_iff_differentiableOn`, `analyticOnNhd_univ_iff_differentiable`, `analyticOn_iff_differentiableOn`, `analyticOn_univ_iff_differentiable`, `circleIntegral_div_sub_of_differentiable_on_off_countable`, `circleIntegral_eq_of_differentiable_on_annulus_off_countable`, `circleIntegral_eq_zero_of_differentiable_on_off_countable`, `circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable`, `circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable`, `circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable`, `circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto`, `circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`, `circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux`, `differentiable_on_off_countable_deriv_eq_smul_circleIntegral`, `hasFPowerSeriesOnBall_of_differentiable_off_countable`, `integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn`, `integral_boundary_rect_eq_zero_of_differentiableOn`, `integral_boundary_rect_eq_zero_of_differentiable_on_off_countable`, `integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real`, `integral_boundary_rect_of_differentiableOn_real`, `integral_boundary_rect_of_hasFDerivAt_real_off_countable`, `two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`, `circleIntegral_eq_zero`, `circleIntegral_one_div_sub_center_pow_smul`, `circleIntegral_sub_inv_smul`, `deriv_eq_smul_circleIntegral`, `hasFPowerSeriesOnBall`, `two_pi_i_inv_smul_circleIntegral_sub_inv_smul`, `analyticAt`, `contDiff`, `hasFPowerSeriesOnBall`, `analyticAt`, `analyticOn`, `analyticOnNhd`, `circleIntegral_one_div_sub_center_pow_smul`, `circleIntegral_sub_inv_smul`, `contDiffOn`, `deriv`, `deriv_eq_smul_circleIntegral`, `hasFPowerSeriesOnBall`	41
Total	41

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt_iff_eventually_differentiableAt` 📖	mathematical	—	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Filter.Eventually` `DifferentiableAt` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `SeminormedAddCommGroup.toPseudoMetricSpace` `nhds`	—	`Filter.mp_mem` `AnalyticAt.eventually_analyticAt` `Filter.univ_mem'` `AnalyticAt.differentiableAt` `eventually_nhds_iff` `DifferentiableOn.analyticOnNhd` `DifferentiableAt.differentiableWithinAt`
`analyticOnNhd_iff_differentiableOn` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	`AnalyticOnNhd` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DifferentiableOn` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`AnalyticOnNhd.differentiableOn` `DifferentiableOn.analyticAt` `IsOpen.mem_nhds`
`analyticOnNhd_univ_iff_differentiable` 📖	mathematical	—	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.univ` `Differentiable` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`analyticOnNhd_iff_differentiableOn` `isOpen_univ`
`analyticOn_iff_differentiableOn` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	`AnalyticOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DifferentiableOn` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`IsOpen.analyticOn_iff_analyticOnNhd` `analyticOnNhd_iff_differentiableOn`
`analyticOn_univ_iff_differentiable` 📖	mathematical	—	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.univ` `Differentiable` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`analyticOn_univ` `analyticOnNhd_univ_iff_differentiable`
`circleIntegral_div_sub_of_differentiable_on_off_countable` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf`	`circleIntegral` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `div_eq_inv_mul` `circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` `instCompleteSpace`
`circleIntegral_eq_of_differentiable_on_annulus_off_countable` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instSDiff` `Metric.closedBall` `Metric.ball` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral`	—	`circleIntegral.integral_sub_inv_smul_sub_smul` `circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn_id` `continuousOn_const` `DifferentiableAt.smul` `IsScalarTower.left` `DifferentiableAt.sub_const` `differentiableAt_id`
`circleIntegral_eq_zero_of_differentiable_on_off_countable` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LE.le.eq_or_lt` `circleIntegral.integral_radius_zero` `Nat.instAtLeastTwoHAddOfNat` `circleIntegral.integral_sub_inv_smul_sub_smul` `circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn_id` `continuousOn_const` `DifferentiableAt.smul` `IsScalarTower.left` `DifferentiableAt.sub_const` `differentiableAt_id` `sub_self` `zero_smul` `smul_zero` `deriv_circleMap` `MeasureTheory.integral_def`
`circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `Nat.factorial` `iteratedDeriv`	—	`LT.lt.le` `HasFPowerSeriesOnBall.factorial_smul` `hasFPowerSeriesOnBall_of_differentiable_off_countable` `Nat.instAtLeastTwoHAddOfNat` `one_smul` `Finset.prod_const_one` `iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod` `cauchyPowerSeries_apply` `Nat.cast_smul_eq_nsmul` `SemigroupAction.mul_smul` `div_mul_cancel₀` `Nat.cast_zero` `instCharZero` `Nat.factorial_ne_zero` `mul_inv_cancel₀` `two_pi_I_ne_zero` `pow_succ` `mul_comm` `one_div` `mul_inv_rev` `inv_pow`
`circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instSDiff` `Metric.closedBall` `Metric.ball` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instInv` `instSub`	—	`Real.exp_log` `LT.lt.trans_le` `Nat.instAtLeastTwoHAddOfNat` `Differentiable.const_add` `differentiable_exp` `Set.Countable.preimage_cexp` `Set.Countable.preimage` `add_right_injective` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `dist_self_add_left` `norm_exp` `sup_of_le_right` `Real.exp_le_exp` `inf_of_le_left` `ContinuousOn.comp` `Continuous.continuousOn` `Differentiable.continuous` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `DifferentiableAt.comp` `ofReal_exp` `intervalIntegral.integral_smul` `NormedSpace.toNormSMulClass` `SMulCommClass.complexToReal` `smulCommClass_self` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `MulZeroClass.zero_mul` `add_zero` `ofReal_mul` `exp_periodic` `sub_self` `zero_add` `integral_boundary_rect_eq_zero_of_differentiable_on_off_countable` `deriv_circleMap` `circleMap_sub_center` `smul_smul` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `circleMap_ne_center` `LT.lt.ne'` `Real.exp_pos`
`circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instInv` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto` `ContinuousOn.mono` `Set.diff_subset` `ContinuousAt.continuousWithinAt` `ContinuousOn.continuousAt` `Metric.closedBall_mem_nhds`
`circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instSDiff` `Metric.closedBall` `Set.instSingletonSet` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Filter.Tendsto` `nhdsWithin` `Compl.compl` `Set.instCompl` `nhds`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instInv` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_zero` `norm_le_zero_iff` `le_of_forall_gt_imp_ge_of_dense` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.HasBasis.tendsto_iff` `nhdsWithin_hasBasis` `Metric.nhds_basis_closedBall` `Metric.nhds_basis_ball` `div_pos` `Real.two_pi_pos` `lt_min` `min_le_left` `min_le_right` `Set.diff_subset_diff_right` `Set.singleton_subset_iff` `Metric.mem_ball_self` `Metric.mem_closedBall_self` `LT.lt.le` `LT.lt.ne'` `dist_self` `circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable` `ContinuousOn.mono` `circleIntegral.integral_smul_const` `circleIntegral.integral_sub_center_inv` `smul_sub` `ContinuousOn.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn_id` `continuousOn_const` `sub_ne_zero` `circleIntegral.integral_sub` `ContinuousOn.circleIntegrable` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.subset_inter` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.sphere_subset_closedBall` `Metric.closedBall_subset_closedBall` `circleIntegral.norm_integral_le_of_norm_le_const` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `dist_eq_norm` `Metric.mem_sphere` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `mem_closedBall_iff_norm` `inv_nonneg` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `ne_of_gt` `Real.pi_pos` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one`
`circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instInv` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` `smul_inv_smul₀` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `instCharZero`
`circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Set.instSDiff` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instInv` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`LE.le.trans_lt` `dist_nonneg` `Set.Countable.insert` `continuousOn_dslope` `Metric.closedBall_mem_nhds_of_mem` `differentiableAt_dslope_of_ne` `Set.mem_insert` `Set.diff_subset_diff_right` `Set.subset_insert` `circleIntegral_eq_zero_of_differentiable_on_off_countable` `LT.lt.le` `ne_of_lt` `Function.update_of_ne` `smul_sub` `ContinuousOn.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn_id` `continuousOn_const` `sub_ne_zero` `Nat.instAtLeastTwoHAddOfNat` `circleIntegral.integral_sub_inv_of_mem_ball` `circleIntegral.integral_smul_const` `sub_eq_zero` `circleIntegral.integral_sub` `ContinuousOn.circleIntegrable` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.mono` `Metric.sphere_subset_closedBall` `circleIntegral.integral_congr`
`differentiable_on_off_countable_deriv_eq_smul_circleIntegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `instSub` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `deriv`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `Nat.cast_one` `div_one` `iteratedDeriv_one` `circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable`
`hasFPowerSeriesOnBall_of_differentiable_off_countable` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `NNReal.toReal` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`HasFPowerSeriesOnBall` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.innerProductSpace` `cauchyPowerSeries` `ENNReal.ofNNReal`	—	`le_radius_cauchyPowerSeries` `ENNReal.coe_pos` `Nat.instAtLeastTwoHAddOfNat` `two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` `HasFPowerSeriesOnBall.hasSum` `hasFPowerSeriesOn_cauchy_integral` `ContinuousOn.circleIntegrable` `ContinuousOn.mono` `Metric.sphere_subset_closedBall`
`integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `reProdIm` `Set.uIcc` `Real` `Real.lattice` `re` `im` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Set.Ioo` `Real.instPreorder` `Real.instMin` `Real.instMax`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `intervalIntegral` `NormedSpace.complexToReal` `instAdd` `ofReal` `instMul` `I` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`integral_boundary_rect_eq_zero_of_differentiable_on_off_countable` `Set.countable_empty` `DifferentiableOn.differentiableAt` `IsOpen.mem_nhds` `IsOpen.reProdIm` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`integral_boundary_rect_eq_zero_of_differentiableOn` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `reProdIm` `Set.uIcc` `Real` `Real.lattice` `re` `im`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `intervalIntegral` `NormedSpace.complexToReal` `instAdd` `ofReal` `instMul` `I` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn` `DifferentiableOn.continuousOn` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `DifferentiableOn.mono` `Set.inter_subset_inter` `Set.preimage_mono` `Set.Ioo_subset_Icc_self`
`integral_boundary_rect_eq_zero_of_differentiable_on_off_countable` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `reProdIm` `Set.uIcc` `Real` `Real.lattice` `re` `im` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `intervalIntegral` `NormedSpace.complexToReal` `instAdd` `ofReal` `instMul` `I` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LinearMap.IsScalarTower.compatibleSMul'` `IsScalarTower.complexToReal` `IsScalarTower.left` `integral_boundary_rect_of_hasFDerivAt_real_off_countable` `HasFDerivAt.restrictScalars` `IsScalarTower.right` `DifferentiableAt.hasFDerivAt` `FiniteDimensional.rclike_to_real` `borelSpace` `fderiv_eq_smul_deriv` `one_smul` `sub_self` `enorm_zero` `intervalIntegral.integral_zero`
`integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `reProdIm` `Set.uIcc` `Real` `Real.lattice` `re` `im` `HasFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `NormedSpace.complexToReal` `MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `I` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `instOne` `MeasureTheory.MeasureSpace.volume`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `intervalIntegral` `instAdd` `ofReal` `instMul` `Real.measureSpace`	—	`FiniteDimensional.rclike_to_real` `borelSpace` `integral_boundary_rect_of_hasFDerivAt_real_off_countable` `Set.countable_empty`
`integral_boundary_rect_of_differentiableOn_real` 📖	mathematical	`DifferentiableOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `SeminormedAddCommGroup.toPseudoMetricSpace` `reProdIm` `Set.uIcc` `Real.lattice` `re` `im` `MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `I` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderiv` `instOne` `MeasureTheory.MeasureSpace.volume`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `intervalIntegral` `instAdd` `ofReal` `instMul` `Real.measureSpace`	—	`FiniteDimensional.rclike_to_real` `borelSpace` `integral_boundary_rect_of_hasFDerivAt_real_off_countable` `Set.countable_empty` `DifferentiableOn.continuousOn` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DifferentiableOn.hasFDerivAt` `interior_reProdIm` `interior_Icc` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMaxOrderOfNontrivial`
`integral_boundary_rect_of_hasFDerivAt_real_off_countable` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `reProdIm` `Set.uIcc` `Real` `Real.lattice` `re` `im` `HasFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `NormedSpace.complexToReal` `MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `I` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `instOne` `MeasureTheory.MeasureSpace.volume`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `intervalIntegral` `instAdd` `ofReal` `instMul` `Real.measureSpace`	—	`FiniteDimensional.rclike_to_real` `borelSpace` `RingHomInvPair.ids` `mk_eq_add_mul_I` `RingHomCompTriple.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.complexToReal` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `neg_add_eq_sub` `neg_sub` `ContinuousOn.comp` `Set.uIcc_comm` `ContinuousLinearEquiv.continuousOn` `Eq.ge` `HasFDerivAt.comp` `max_comm` `min_comm` `ContinuousLinearEquiv.hasFDerivAt` `NormedSpace.toNormSMulClass` `intervalIntegral.integral_symm` `MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable` `Set.Countable.preimage` `ContinuousLinearEquiv.injective` `ContinuousOn.neg` `IsTopologicalAddGroup.toContinuousNeg` `ContinuousOn.const_smul` `HasFDerivAt.neg` `HasFDerivAt.const_smul` `MeasureTheory.Integrable.neg` `MeasureTheory.MeasurePreserving.integrableOn_comp_preimage` `MeasureTheory.MeasurePreserving.symm` `volume_preserving_equiv_real_prod` `MeasurableEquiv.measurableEmbedding`
`two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instInv` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `circleIntegral` `instSub`	—	`LE.le.trans_lt` `dist_nonneg` `mem_closure_iff_nhds` `Continuous.tendsto'` `Continuous.fun_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_const` `continuous_ofReal` `add_zero` `mem_nhds_iff_exists_Ioo_subset` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMinOrderOfNontrivial` `Filter.inter_mem` `IsOpen.mem_nhds` `Metric.isOpen_ball` `Set.diff_nonempty` `Set.Countable.mono` `Set.Countable.preimage` `add_right_injective` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `ofReal_injective` `LE.le.not_gt` `Cardinal.mk_Ioo_real` `LT.lt.trans` `Cardinal.le_aleph0_iff_set_countable` `Cardinal.aleph0_lt_continuum` `Nat.instAtLeastTwoHAddOfNat` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `hasFPowerSeriesOn_cauchy_integral` `ContinuousOn.circleIntegrable` `NNReal.coe_nonneg` `ContinuousOn.mono` `Metric.sphere_subset_closedBall` `ContinuousOn.continuousAt` `HasFPowerSeriesOnBall.continuousOn` `Metric.isOpen_eball` `Metric.eball_coe` `Metric.closedBall_mem_nhds_of_mem` `tendsto_nhds_unique_of_frequently_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.Frequently.mono` `mem_closure_iff_frequently` `circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux` `inv_smul_smul₀` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `instCharZero`

DiffContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleIntegral_eq_zero` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `DiffContOnCl` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`circleIntegral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable` `Set.countable_empty` `continuousOn_ball` `differentiableAt` `Metric.isOpen_ball`
`circleIntegral_one_div_sub_center_pow_smul` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DiffContOnCl` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Monoid.toNatPow` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Nat.factorial` `iteratedDeriv`	—	`Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable` `Set.countable_empty` `continuousOn_ball` `differentiableAt` `Metric.isOpen_ball`
`circleIntegral_sub_inv_smul` 📖	mathematical	`DiffContOnCl` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instInv` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` `Set.countable_empty` `continuousOn_ball` `differentiableAt` `Metric.isOpen_ball`
`deriv_eq_smul_circleIntegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DiffContOnCl` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Monoid.toNatPow` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `deriv` `NormedAddCommGroup.toAddCommGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `Nat.cast_one` `div_one` `iteratedDeriv_one` `circleIntegral_one_div_sub_center_pow_smul`
`hasFPowerSeriesOnBall` 📖	mathematical	`DiffContOnCl` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NNReal.toReal` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`HasFPowerSeriesOnBall` `cauchyPowerSeries` `ENNReal.ofNNReal`	—	`Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable` `Set.countable_empty` `continuousOn_ball` `differentiableAt` `Metric.isOpen_ball`
`two_pi_i_inv_smul_circleIntegral_sub_inv_smul` 📖	mathematical	`DiffContOnCl` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instInv` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `circleIntegral` `Complex.instSub`	—	`not_le` `Iff.not` `Metric.ball_eq_empty` `Set.Nonempty.ne_empty` `Set.nonempty_of_mem` `Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable` `Set.countable_empty` `closure_ball` `LT.lt.ne` `continuousOn` `Set.diff_empty` `differentiableAt` `Metric.isOpen_ball`

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	`AnalyticAt` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`DifferentiableOn.analyticAt` `differentiableOn` `Filter.univ_mem`
`contDiff` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContDiff` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`contDiff_iff_contDiffAt` `AnalyticAt.contDiffAt` `analyticAt`
`hasFPowerSeriesOnBall` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`HasFPowerSeriesOnBall` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace` `cauchyPowerSeries` `NNReal.toReal` `Top.top` `ENNReal` `instTopENNReal`	—	`HasFPowerSeriesOnBall.r_eq_top_of_exists` `DifferentiableOn.hasFPowerSeriesOnBall` `differentiableOn` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Filter` `Filter.instMembership` `nhds`	`AnalyticAt` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`Filter.HasBasis.mem_iff` `Metric.nhds_basis_closedBall` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `HasFPowerSeriesOnBall.analyticAt` `hasFPowerSeriesOnBall` `mono`
`analyticOn` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsOpen`	`AnalyticOn` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`AnalyticOnNhd.analyticOn` `analyticOnNhd`
`analyticOnNhd` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsOpen`	`AnalyticOnNhd` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`analyticAt` `IsOpen.mem_nhds`
`circleIntegral_one_div_sub_center_pow_smul` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Monoid.toNatPow` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Nat.factorial` `iteratedDeriv`	—	`DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul` `diffContOnCl` `mono` `Metric.closure_ball_subset_closedBall`
`circleIntegral_sub_inv_smul` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Set` `Set.instMembership` `Metric.ball`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instInv` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`DiffContOnCl.circleIntegral_sub_inv_smul` `diffContOnCl` `mono` `Metric.closure_ball_subset_closedBall`
`contDiffOn` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsOpen`	`ContDiffOn` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`AnalyticOnNhd.contDiffOn_of_completeSpace` `analyticOnNhd`
`deriv` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsOpen`	`deriv`	—	`AnalyticOnNhd.differentiableOn` `AnalyticOnNhd.deriv` `analyticOnNhd`
`deriv_eq_smul_circleIntegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall`	`circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Monoid.toNatPow` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `deriv`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `Nat.cast_one` `div_one` `iteratedDeriv_one` `circleIntegral_one_div_sub_center_pow_smul`
`hasFPowerSeriesOnBall` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `NNReal.toReal` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`HasFPowerSeriesOnBall` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace` `cauchyPowerSeries` `ENNReal.ofNNReal`	—	`DiffContOnCl.hasFPowerSeriesOnBall` `diffContOnCl` `mono` `Metric.closure_ball_subset_closedBall`

---

← Back to Index