Documentation Verification Report

TaylorSeries

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

Statistics

Metric	Count
Definitions	0
Theorems `hasSum_taylorSeries_of_entire`, `hasSum_taylorSeries_on_ball`, `hasSum_taylorSeries_on_eball`, `hasSum_taylorSeries_on_emetric_ball`, `taylorSeries_eq_of_entire`, `taylorSeries_eq_of_entire'`, `taylorSeries_eq_on_ball`, `taylorSeries_eq_on_ball'`, `taylorSeries_eq_on_eball`, `taylorSeries_eq_on_eball'`, `taylorSeries_eq_on_emetric_ball`, `taylorSeries_eq_on_emetric_ball'`	12
Total	12

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_taylorSeries_of_entire` 📖	mathematical	`Differentiable` `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`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`hasSum_taylorSeries_on_eball` `Differentiable.differentiableOn` `Metric.mem_eball` `edist_lt_top`
`hasSum_taylorSeries_on_ball` 📖	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` `Metric.ball` `Set` `Set.instMembership`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Metric.mem_ball'` `Metric.pos_of_mem_ball` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `Metric.eball_coe` `sub_zero` `HasFPowerSeriesOnBall.hasSum_iteratedFDeriv` `DifferentiableOn.hasFPowerSeriesOnBall` `DifferentiableOn.mono` `Metric.closedBall_subset_ball` `instCharZero` `Finset.prod_const` `Finset.card_fin` `mul_one` `ContinuousMultilinearMap.map_smul_univ` `add_sub_cancel`
`hasSum_taylorSeries_on_eball` 📖	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` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `Set` `Set.instMembership`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`exists_between` `ENNReal.instDenselyOrdered` `Metric.mem_eball'` `CanLift.prf` `ENNReal.canLift` `ne_top_of_lt` `hasSum_taylorSeries_on_ball` `Metric.eball_coe` `DifferentiableOn.mono` `Metric.eball_subset_eball` `LT.lt.le`
`hasSum_taylorSeries_on_emetric_ball` 📖	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` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `Set` `Set.instMembership`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`hasSum_taylorSeries_on_eball`
`taylorSeries_eq_of_entire` 📖	mathematical	`Differentiable` `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`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_taylorSeries_of_entire`
`taylorSeries_eq_of_entire'` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `instMul` `instInv` `instNatCast` `Nat.factorial` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instSub` `SummationFilter.unconditional`	—	`mul_right_comm` `smul_eq_mul` `mul_assoc` `taylorSeries_eq_of_entire` `instCompleteSpace`
`taylorSeries_eq_on_ball` 📖	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` `Metric.ball` `Set` `Set.instMembership`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_taylorSeries_on_ball`
`taylorSeries_eq_on_ball'` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `instMul` `instInv` `instNatCast` `Nat.factorial` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instSub` `SummationFilter.unconditional`	—	`mul_right_comm` `smul_eq_mul` `mul_assoc` `taylorSeries_eq_on_ball` `instCompleteSpace`
`taylorSeries_eq_on_eball` 📖	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` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `Set` `Set.instMembership`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_taylorSeries_on_eball`
`taylorSeries_eq_on_eball'` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `instNormedField` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `instMul` `instInv` `instNatCast` `Nat.factorial` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instSub` `SummationFilter.unconditional`	—	`mul_right_comm` `smul_eq_mul` `mul_assoc` `taylorSeries_eq_on_eball` `instCompleteSpace`
`taylorSeries_eq_on_emetric_ball` 📖	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` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `Set` `Set.instMembership`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField` `instInv` `instNatCast` `Nat.factorial` `Monoid.toPow` `instSub` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `SummationFilter.unconditional`	—	`taylorSeries_eq_on_eball`
`taylorSeries_eq_on_emetric_ball'` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `instNormedField` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `instMul` `instInv` `instNatCast` `Nat.factorial` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instSub` `SummationFilter.unconditional`	—	`taylorSeries_eq_on_eball'`

---

← Back to Index