Documentation Verification Report

IteratedFDeriv

📁 Source: Mathlib/Analysis/Analytic/IteratedFDeriv.lean

Statistics

Metric	Count
Definitions `iteratedFDerivSeries`	1
Theorems `domDomCongr_iteratedFDeriv`, `domDomCongr_iteratedFDerivWithin`, `iteratedFDerivWithin_comp_perm`, `iteratedFDeriv_comp_perm`, `domDomCongr_iteratedFDeriv`, `iteratedFDeriv_comp_perm`, `domDomCongr_iteratedFDerivWithin`, `iteratedFDerivWithin_comp_perm`, `iteratedFDeriv_comp_diagonal`, `iteratedFDerivSeries_eq_zero`, `iteratedFDeriv_eq_sum`, `iteratedFDeriv_eq_sum_of_completeSpace`, `iteratedFDerivWithin`, `iteratedFDerivWithin_eq_sum`, `iteratedFDerivWithin_eq_sum_of_completeSpace`, `iteratedFDerivWithin_eq_zero`	16
Total	17

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domDomCongr_iteratedFDeriv` 📖	mathematical	`AnalyticOn` `Set.univ`	`ContinuousMultilinearMap.domDomCongr` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `iteratedFDeriv`	—	`iteratedFDerivWithin_univ` `domDomCongr_iteratedFDerivWithin` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`domDomCongr_iteratedFDerivWithin` 📖	mathematical	`AnalyticOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`ContinuousMultilinearMap.domDomCongr` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `iteratedFDerivWithin`	—	`ContinuousMultilinearMap.ext` `iteratedFDerivWithin_comp_perm`
`iteratedFDerivWithin_comp_perm` 📖	mathematical	`AnalyticOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum` `Equiv.sum_comp` `Finset.sum_congr`
`iteratedFDeriv_comp_perm` 📖	mathematical	`AnalyticOn` `Set.univ`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`iteratedFDerivWithin_univ` `iteratedFDerivWithin_comp_perm` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domDomCongr_iteratedFDeriv` 📖	mathematical	`ContDiffAt` `Top.top` `WithTop` `ENat` `WithTop.top`	`ContinuousMultilinearMap.domDomCongr` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `iteratedFDeriv`	—	`iteratedFDerivWithin_univ` `ContDiffWithinAt.domDomCongr_iteratedFDerivWithin` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`iteratedFDeriv_comp_perm` 📖	mathematical	`ContDiffAt` `Top.top` `WithTop` `ENat` `WithTop.top`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`iteratedFDerivWithin_univ` `ContDiffWithinAt.iteratedFDerivWithin_comp_perm` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domDomCongr_iteratedFDerivWithin` 📖	mathematical	`ContDiffWithinAt` `Top.top` `WithTop` `ENat` `WithTop.top` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`ContinuousMultilinearMap.domDomCongr` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `iteratedFDerivWithin`	—	`ContinuousMultilinearMap.ext` `iteratedFDerivWithin_comp_perm`
`iteratedFDerivWithin_comp_perm` 📖	mathematical	`ContDiffWithinAt` `Top.top` `WithTop` `ENat` `WithTop.top` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`contDiffOn'` `le_rfl` `iteratedFDerivWithin_inter_open` `AnalyticOn.iteratedFDerivWithin_comp_perm` `ContDiffOn.analyticOn` `Set.insert_eq_of_mem` `UniqueDiffOn.inter` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`

ContinuousMultilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iteratedFDeriv_comp_diagonal` 📖	mathematical	—	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike` `iteratedFDeriv` `Finset.sum` `Equiv.Perm` `Finset.univ` `Equiv.instFintype` `Fin.fintype` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.sum_comp` `ContinuousLinearMap.iteratedFDeriv_comp_right` `contDiff` `le_rfl` `iteratedFDeriv_eq` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.sum_congr` `sum_apply` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `iteratedFDerivComponent_apply` `Finite.of_fintype` `Fintype.bijective_iff_injective_and_card` `Function.Embedding.injective` `Function.Bijective.surjective` `Function.instEmbeddingLikeEmbedding` `Function.Embedding.toEquivRange_symm_apply_self` `Equiv.ofBijective_symm_apply_apply`

FormalMultilinearSeries

Definitions

Name	Category	Theorems
`iteratedFDerivSeries` 📖	CompOp	2 math math: `iteratedFDerivSeries_eq_zero`, `HasFPowerSeriesWithinOnBall.iteratedFDerivWithin`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iteratedFDerivSeries_eq_zero` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`iteratedFDerivSeries` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `ContinuousMultilinearMap.ext` `congr_zero` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `derivSeries_eq_zero`

HasFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iteratedFDeriv_eq_sum` 📖	mathematical	`HasFPowerSeriesOnBall` `AnalyticOn` `Set.univ`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Finset.sum` `Equiv.Perm` `Finset.univ` `Equiv.instFintype` `Fin.fintype` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `Set.mem_univ`
`iteratedFDeriv_eq_sum_of_completeSpace` 📖	mathematical	`HasFPowerSeriesOnBall`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Finset.sum` `Equiv.Perm` `Finset.univ` `Equiv.instFintype` `Fin.fintype` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `Set.mem_univ`

HasFPowerSeriesWithinOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iteratedFDerivWithin` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `AnalyticOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDerivWithin` `FormalMultilinearSeries.iteratedFDerivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall` `RingHomInvPair.ids` `RingHomIsometric.ids` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `iteratedFDerivWithin_succ_eq_comp_left` `fderivWithin_of_mem_of_analyticOn` `AnalyticOn.iteratedFDerivWithin`
`iteratedFDerivWithin_eq_sum` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `AnalyticOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Finset.sum` `Equiv.Perm` `Finset.univ` `Equiv.instFintype` `Fin.fintype` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDerivWithin_inter_open` `Metric.isOpen_eball` `Metric.mem_eball_self` `r_pos` `mono` `Set.inter_subset_left` `AnalyticOn.mono` `UniqueDiffOn.inter` `Set.inter_subset_right`
`iteratedFDerivWithin_eq_sum_of_completeSpace` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Finset.sum` `Equiv.Perm` `Finset.univ` `Equiv.instFintype` `Fin.fintype` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDerivWithin_inter_open` `Metric.isOpen_eball` `Metric.mem_eball_self` `r_pos` `mono` `Set.inter_subset_left` `AnalyticOn.mono` `analyticOn` `Set.insert_eq_of_mem` `subset_refl` `Set.instReflSubset` `UniqueDiffOn.inter` `Set.inter_subset_right`
`iteratedFDerivWithin_eq_zero` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `AnalyticOn` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instZero`	`iteratedFDerivWithin`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `coeff_zero` `iteratedFDerivWithin` `FormalMultilinearSeries.iteratedFDerivSeries_eq_zero` `FormalMultilinearSeries.congr_zero` `ContinuousMultilinearMap.zero_apply`

---

← Back to Index