Documentation Verification Report

Analytic

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Statistics

Metric	Count
Definitions	0
Theorems `deriv`, `differentiableAt`, `differentiableWithinAt`, `fderiv`, `hasStrictDerivAt`, `hasStrictFDerivAt`, `iterated_deriv`, `differentiableOn`, `exists_hasFTaylorSeriesUpToOn`, `fderivWithin`, `hasFTaylorSeriesUpToOn`, `iteratedFDerivWithin`, `deriv`, `deriv_of_isOpen`, `differentiableOn`, `fderiv`, `fderiv_of_isOpen`, `hasFTaylorSeriesUpToOn`, `iteratedFDeriv`, `iteratedFDeriv_of_isOpen`, `iterated_deriv`, `differentiableWithinAt`, `exists_hasFTaylorSeriesUpToOn`, `deriv`, `fderiv`, `iteratedFDeriv`, `iterated_deriv`, `hasFDerivAt_uncurry_of_multilinear`, `changeOriginSeries_support`, `changeOrigin_toFormalMultilinearSeries`, `hasFDerivAt`, `hasFTaylorSeriesUpTo_iteratedFDeriv`, `hasStrictFDerivAt`, `hasStrictFDerivAt_uncurry`, `iteratedFDeriv_eq`, `norm_iteratedFDeriv_le`, `derivSeries_apply_diag`, `derivSeries_coeff_one`, `continuousMultilinearMap_apply`, `linear_multilinear_comp`, `multilinear_comp`, `continuousMultilinearMap_apply`, `linear_multilinear_comp`, `multilinear_comp`, `deriv`, `differentiableAt`, `eventually_differentiableAt`, `fderiv_eq`, `hasDerivAt`, `hasFDerivAt`, `hasStrictDerivAt`, `hasStrictFDerivAt`, `differentiableOn`, `factorial_smul`, `fderiv`, `fderiv_eq`, `hasFDerivAt`, `hasSum_iteratedFDeriv`, `iteratedFDeriv_zero_apply_diag`, `differentiableWithinAt`, `fderivWithin_eq`, `hasFDerivWithinAt`, `hasStrictFDerivWithinAt`, `differentiableOn`, `fderivWithin`, `fderivWithin_eq`, `fderivWithin_of_mem`, `fderivWithin_of_mem_of_analyticOn`, `hasFDerivWithinAt`, `hasSum_derivSeries_of_hasFDerivWithinAt`, `differentiableOn`, `fderiv`, `fderiv'`, `fderiv_eq`, `hasFDerivAt`, `hasStrictFDerivAt`, `continuousMultilinearMap_apply`, `analyticAt_symm`, `analyticAt_symm'`	79
Total	79

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`exists_ball_analyticOnNhd` `AnalyticOnNhd.deriv` `dist_self`
`differentiableAt` 📖	mathematical	`AnalyticAt`	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`HasFPowerSeriesAt.differentiableAt`
`differentiableWithinAt` 📖	mathematical	`AnalyticAt`	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`DifferentiableAt.differentiableWithinAt` `differentiableAt`
`fderiv` 📖	mathematical	`AnalyticAt`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `HasFPowerSeriesOnBall.analyticAt` `HasFPowerSeriesOnBall.fderiv`
`hasStrictDerivAt` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`HasStrictDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `deriv`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `toSpanSingleton_deriv` `hasStrictFDerivAt`
`hasStrictFDerivAt` 📖	mathematical	`AnalyticAt`	`HasStrictFDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `fderiv`	—	`RingHomInvPair.ids` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `HasFPowerSeriesAt.fderiv_eq` `HasFPowerSeriesAt.hasStrictFDerivAt`
`iterated_deriv` 📖	mathematical	`AnalyticAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Function.iterate_succ'` `deriv`

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableOn` 📖	mathematical	`AnalyticOn`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`DifferentiableWithinAt.mono` `AnalyticWithinAt.differentiableWithinAt`
`exists_hasFTaylorSeriesUpToOn` 📖	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`	`HasFTaylorSeriesUpToOn` `Top.top` `WithTop` `ENat` `WithTop.top` `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`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `hasFTaylorSeriesUpToOn` `iteratedFDerivWithin`
`fderivWithin` 📖	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`	`ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin`	—	`RingHomIsometric.ids` `smulCommClass_self` `HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn`
`hasFTaylorSeriesUpToOn` 📖	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`	`HasFTaylorSeriesUpToOn` `ftaylorSeriesWithin`	—	`smulCommClass_self` `DifferentiableWithinAt.hasFDerivWithinAt` `AnalyticWithinAt.differentiableWithinAt` `iteratedFDerivWithin` `Set.insert_eq_of_mem` `AnalyticWithinAt.continuousWithinAt`
`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`	`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`	—	`smulCommClass_self` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDerivWithin_zero_eq_comp` `ContinuousLinearMap.comp_analyticOn` `IsTopologicalAddGroup.toContinuousAdd` `RingHomIsometric.ids` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `iteratedFDerivWithin_succ_eq_comp_left` `AnalyticOnNhd.comp_analyticOn` `LinearIsometryEquiv.analyticOnNhd` `fderivWithin` `Set.mapsTo_univ`

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ContinuousLinearMap.comp_analyticOnNhd` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `fderiv`
`deriv_of_isOpen` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ContinuousLinearMap.comp_analyticOnNhd` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `fderiv_of_isOpen`
`differentiableOn` 📖	mathematical	`AnalyticOnNhd`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`AnalyticAt.differentiableWithinAt`
`fderiv` 📖	mathematical	`AnalyticOnNhd`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`AnalyticAt.fderiv`
`fderiv_of_isOpen` 📖	mathematical	`AnalyticOnNhd` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `IsOpen.analyticOn_iff_analyticOnNhd` `AnalyticOn.congr` `AnalyticOn.fderivWithin` `IsOpen.uniqueDiffOn` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fderivWithin_of_isOpen`
`hasFTaylorSeriesUpToOn` 📖	mathematical	`AnalyticOnNhd`	`HasFTaylorSeriesUpToOn` `ftaylorSeries`	—	`HasFDerivAt.hasFDerivWithinAt` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `DifferentiableAt.hasFDerivAt` `AnalyticAt.differentiableAt` `iteratedFDeriv` `ContinuousAt.continuousWithinAt` `DifferentiableAt.continuousAt` `IsBoundedSMul.continuousSMul` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instContinuousSMul`
`iteratedFDeriv` 📖	mathematical	`AnalyticOnNhd`	`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.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv`	—	`smulCommClass_self` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDeriv_zero_eq_comp` `ContinuousLinearMap.comp_analyticOnNhd` `IsTopologicalAddGroup.toContinuousAdd` `RingHomIsometric.ids` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `iteratedFDeriv_succ_eq_comp_left` `fderiv` `ContinuousMultilinearMap.instCompleteSpace` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsBoundedSMul.continuousSMul` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.instFirstCountableTopologyForallOfCountable` `instCountableFin` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace`
`iteratedFDeriv_of_isOpen` 📖	mathematical	`AnalyticOnNhd` `IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv`	—	`smulCommClass_self` `IsOpen.analyticOn_iff_analyticOnNhd` `AnalyticOn.congr` `AnalyticOn.iteratedFDerivWithin` `IsOpen.uniqueDiffOn` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin_of_isOpen`
`iterated_deriv` 📖	mathematical	`AnalyticOnNhd` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Function.iterate_succ'` `deriv`

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableWithinAt` 📖	mathematical	`AnalyticWithinAt`	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInsert`	—	`HasFPowerSeriesWithinAt.differentiableWithinAt`
`exists_hasFTaylorSeriesUpToOn` 📖	mathematical	`AnalyticWithinAt`	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.instInsert` `HasFTaylorSeriesUpToOn` `AnalyticOn` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `exists_analyticAt` `AnalyticAt.exists_mem_nhds_analyticOnNhd` `inter_mem_nhdsWithin` `AnalyticOnNhd.hasFTaylorSeriesUpToOn` `AnalyticOnNhd.mono` `Set.inter_subset_right` `HasFTaylorSeriesUpToOn.congr` `AnalyticOn.mono` `AnalyticOnNhd.analyticOn` `AnalyticOnNhd.iteratedFDeriv`

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv` 📖	mathematical	`CPolynomialOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ContinuousLinearMap.comp_cpolynomialOn` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `fderiv`
`fderiv` 📖	mathematical	`CPolynomialOn`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `HasFiniteFPowerSeriesOnBall.cpolynomialAt` `HasFiniteFPowerSeriesOnBall.fderiv'`
`iteratedFDeriv` 📖	mathematical	`CPolynomialOn`	`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.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv`	—	`smulCommClass_self` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDeriv_zero_eq_comp` `ContinuousLinearMap.comp_cpolynomialOn` `IsTopologicalAddGroup.toContinuousAdd` `RingHomIsometric.ids` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `iteratedFDeriv_succ_eq_comp_left` `fderiv`
`iterated_deriv` 📖	mathematical	`CPolynomialOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Nat.iterate` `deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Function.iterate_succ'` `deriv`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFDerivAt_uncurry_of_multilinear` 📖	mathematical	—	`HasFDerivAt` `Prod.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `Pi.addCommGroup` `Prod.instModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Pi.module` `instTopologicalSpaceProd` `Pi.topologicalSpace` `DFunLike.coe` `ContinuousMultilinearMap` `ContinuousMultilinearMap.funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `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` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `funLike` `Prod.instAddCommMonoid` `add` `comp` `RingHomCompTriple.ids` `addCommMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `module` `topologicalSpace` `flipMultilinear` `fst` `Finset.sum` `Finset.univ` `ContinuousMultilinearMap.toContinuousLinearMap` `proj` `snd`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `HasFDerivAt.continuousMultilinearMap_apply` `RingHomCompTriple.ids` `hasFDerivAt` `hasFDerivAt_pi'` `Finite.of_fintype` `hasFDerivAt_snd`

ContinuousMultilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`changeOriginSeries_support` 📖	mathematical	—	`FormalMultilinearSeries.changeOriginSeries` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `toFormalMultilinearSeries` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ContinuousMultilinearMap` `addCommMonoid` `instModule` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `instZero`	—	`Finset.sum_eq_zero` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `LinearIsometryEquiv.map_zero` `RingHomInvPair.ids` `instContinuousConstSMul` `instSMulCommClass`
`changeOrigin_toFormalMultilinearSeries` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.normedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Pi.normedSpace` `ContinuousLinearMap` `seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin` `toFormalMultilinearSeries` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `linearDeriv`	—	`ContinuousLinearMap.ext` `RingHomInvPair.ids` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `continuousMultilinearCurryFin1_apply` `linearDeriv_apply` `FormalMultilinearSeries.changeOrigin.eq_1` `FormalMultilinearSeries.sum.eq_1` `isEmpty_or_nonempty` `add_comm` `Fintype.card_eq_zero` `Fintype.sum_empty` `changeOriginSeries_support` `zero_apply` `tsum_zero` `tsum_eq_single` `SummationFilter.instLeAtTopUnconditional` `eq_tsub_iff_add_eq_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Fintype.card_pos` `FormalMultilinearSeries.changeOriginSeries.eq_1` `sum_apply` `Fin.snoc_zero` `Finset.sum_congr` `FormalMultilinearSeries.changeOriginSeriesTerm_apply` `Fintype.sum_bijective` `Finset.card_compl` `Fintype.card_fin` `Finset.card_singleton` `Function.Bijective.comp` `Finset.singleton_injective` `compl_injective` `Finset.card_eq_one` `compl_eq_comm` `Equiv.bijective` `Finset.compl_singleton` `Finset.piecewise_erase_univ` `toFormalMultilinearSeries.eq_1` `Function.update_apply` `Equiv.injective` `ite_apply`
`hasFDerivAt` 📖	mathematical	—	`HasFDerivAt` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `Pi.module` `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` `Pi.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `ContinuousMultilinearMap` `funLike` `linearDeriv` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`HasStrictFDerivAt.hasFDerivAt` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasStrictFDerivAt`
`hasFTaylorSeriesUpTo_iteratedFDeriv` 📖	mathematical	—	`HasFTaylorSeriesUpTo` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Top.top` `WithTop` `ENat` `WithTop.top` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike` `iteratedFDeriv`	—	`Fin.isEmpty'` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.sum_congr` `Finset.univ_unique` `Finset.sum_singleton` `Matrix.zero_empty` `iteratedFDerivComponent_apply` `Matrix.range_empty` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `instIsTopologicalAddGroup` `RingHomCompTriple.ids` `ContinuousLinearMap.ext` `ext` `sum_apply` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply` `linearDeriv_apply` `Finset.sum_sigma'` `Equiv.sum_comp` `Fin.cons_succ` `Function.Embedding.toEquivRange_symm_apply_self` `Fin.cons_zero` `Function.instEmbeddingLikeEmbedding` `Mathlib.Tactic.Contrapose.contrapose₄` `Set.range_comp_subset_range` `Equiv.embeddingFinSucc_fst` `Function.update_of_ne` `Equiv.embeddingFinSucc_snd` `Set.mem_range_self` `HasFDerivAt.fun_sum` `HasFDerivAt.comp` `hasFDerivAt` `ContinuousLinearMap.hasFDerivAt` `continuous_finset_sum` `Continuous.comp` `coe_continuous` `ContinuousLinearMap.continuous`
`hasStrictFDerivAt` 📖	mathematical	—	`HasStrictFDerivAt` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `Pi.module` `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` `Pi.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `ContinuousMultilinearMap` `funLike` `linearDeriv` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `RingHomIsometric.ids` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `changeOrigin_toFormalMultilinearSeries` `zero_add` `HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt` `hasFiniteFPowerSeriesOnBall` `ENNReal.coe_lt_top`
`hasStrictFDerivAt_uncurry` 📖	mathematical	—	`HasStrictFDerivAt` `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` `Prod.instAddCommGroup` `instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Pi.addCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `Pi.addCommMonoid` `instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Pi.module` `instTopologicalSpaceProd` `instTopologicalSpace` `Pi.topologicalSpace` `DFunLike.coe` `funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `ContinuousLinearMap.add` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `apply` `IsBoundedSMul.continuousSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ContinuousLinearMap.fst` `linearDeriv` `ContinuousLinearMap.snd`	—	`smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomCompTriple.ids` `HasStrictFDerivAt.comp` `hasStrictFDerivAt` `hasStrictFDerivAt_pi` `instFiniteOption` `Finite.of_fintype` `hasStrictFDerivAt_id` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.prod_ext` `ContinuousLinearMap.ext` `eq_or_ne` `Function.update_self` `Function.update_of_ne` `ContinuousLinearMap.add_comp` `linearDeriv_apply` `Finset.sum_congr` `Fintype.sum_option` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `zero_add`
`iteratedFDeriv_eq` 📖	mathematical	—	`iteratedFDeriv` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike` `iteratedFDeriv`	—	`HasFTaylorSeriesUpTo.eq_iteratedFDeriv` `hasFTaylorSeriesUpTo_iteratedFDeriv` `le_top`
`norm_iteratedFDeriv_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.normedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Pi.normedSpace` `hasOpNorm'` `Pi.seminormedAddCommGroup` `Fin.fintype` `iteratedFDeriv` `DFunLike.coe` `funLike` `Real.instMul` `Real.instNatCast` `Nat.descFactorial` `Fintype.card` `hasOpNorm` `Monoid.toNatPow` `Real.instMonoid` `NormedAddCommGroup.toNorm`	—	`iteratedFDeriv_eq` `norm_iteratedFDeriv_le'`

FormalMultilinearSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivSeries_apply_diag` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `ContinuousMultilinearMap` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousMultilinearMap.funLike` `derivSeries` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `ContinuousMultilinearMap.sum_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `RingHomIsometric.ids` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply` `Finset.sum_congr` `Matrix.zero_empty` `Fin.snoc_zero` `changeOriginSeriesTerm_apply` `Finset.piecewise_same` `add_comm` `Fintype.card.eq_1` `Fintype.card_subtype` `Finset.powerset_univ` `Finset.powersetCard_eq_filter` `Finset.card_powersetCard` `Fintype.card_fin` `Nat.choose_succ_self_right` `Finset.sum_const`
`derivSeries_coeff_one` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike` `coeff` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `derivSeries` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	—	`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` `derivSeries_apply_diag`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousMultilinearMap_apply` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace`	`DFunLike.coe` `ContinuousMultilinearMap.funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `ContinuousLinearMap.comp` `ContinuousMultilinearMap.addCommMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `RingHomCompTriple.ids` `ContinuousMultilinearMap.apply` `IsBoundedSMul.continuousSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Finset.sum` `ContinuousLinearMap.addCommMonoid` `Finset.univ` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `HasFDerivWithinAt.continuousMultilinearMap_apply`
`linear_multilinear_comp` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `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` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.funLike` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearMap.addCommMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.flipMultilinear` `Finset.sum` `Finset.univ` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `continuousMultilinearMap_apply` `RingHomCompTriple.ids` `comp` `ContinuousLinearMap.hasFDerivAt`
`multilinear_comp` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `Finset.sum` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.univ` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.comp_zero` `zero_add` `RingHomIsometric.ids` `continuousMultilinearMap_apply` `hasFDerivAt_const`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousMultilinearMap_apply` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace`	`DFunLike.coe` `ContinuousMultilinearMap.funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `ContinuousLinearMap.comp` `ContinuousMultilinearMap.addCommMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `RingHomCompTriple.ids` `ContinuousMultilinearMap.apply` `IsBoundedSMul.continuousSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Finset.sum` `ContinuousLinearMap.addCommMonoid` `Finset.univ` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.ext` `ContinuousLinearMap.coe_sum'` `Finset.sum_congr` `Finset.sum_apply` `ContinuousLinearMap.add_comp` `ContinuousMultilinearMap.linearDeriv_apply` `HasFDerivAt.comp_hasFDerivWithinAt` `HasStrictFDerivAt.hasFDerivAt` `ContinuousMultilinearMap.hasStrictFDerivAt_uncurry` `prodMk` `hasFDerivWithinAt_pi` `Finite.of_fintype`
`linear_multilinear_comp` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `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` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.funLike` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearMap.addCommMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.flipMultilinear` `Finset.sum` `Finset.univ` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `continuousMultilinearMap_apply` `RingHomCompTriple.ids` `HasFDerivAt.comp_hasFDerivWithinAt` `ContinuousLinearMap.hasFDerivAt`
`multilinear_comp` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.funLike` `Finset.sum` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.univ` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.comp_zero` `zero_add` `RingHomIsometric.ids` `continuousMultilinearMap_apply` `hasFDerivWithinAt_const`

HasFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv` 📖	mathematical	`HasFPowerSeriesAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`deriv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousMultilinearMap.funLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`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` `HasDerivAt.deriv` `hasDerivAt`
`differentiableAt` 📖	mathematical	`HasFPowerSeriesAt`	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivAt.differentiableAt` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `hasFDerivAt`
`eventually_differentiableAt` 📖	mathematical	`HasFPowerSeriesAt`	`Filter.Eventually` `DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `DifferentiableOn.eventually_differentiableAt` `HasFPowerSeriesOnBall.differentiableOn` `Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos`
`fderiv_eq` 📖	mathematical	`HasFPowerSeriesAt`	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivAt.fderiv` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt`
`hasDerivAt` 📖	mathematical	`HasFPowerSeriesAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`HasDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousMultilinearMap.funLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`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` `HasStrictDerivAt.hasDerivAt` `hasStrictDerivAt`
`hasFDerivAt` 📖	mathematical	`HasFPowerSeriesAt`	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasStrictFDerivAt.hasFDerivAt` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `hasStrictFDerivAt`
`hasStrictDerivAt` 📖	mathematical	`HasFPowerSeriesAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`HasStrictDerivAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `DFunLike.coe` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousMultilinearMap.funLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`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` `HasStrictFDerivAt.hasStrictDerivAt` `IsBoundedSMul.continuousSMul` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `hasStrictFDerivAt`
`hasStrictFDerivAt` 📖	mathematical	`HasFPowerSeriesAt`	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `Set.insert_eq_of_mem` `Set.univ_prod_univ` `nhdsWithin_univ` `HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt` `hasFPowerSeriesWithinAt`

HasFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableOn` 📖	mathematical	`HasFPowerSeriesOnBall`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `AnalyticAt.differentiableWithinAt` `analyticAt_of_mem`
`factorial_smul` 📖	mathematical	`HasFPowerSeriesOnBall`	`AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Nat.factorial` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `iteratedFDeriv`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Nat.factorial_zero` `one_smul` `iteratedFDeriv_zero_apply_diag` `Nat.factorial_succ` `mul_comm` `SemigroupAction.mul_smul` `smulCommClass_self` `FormalMultilinearSeries.derivSeries_apply_diag` `AddMonoid.nat_smulCommClass'` `AddMonoid.continuousConstSMul_nat` `ContinuousLinearMap.smul_apply` `RingHomIsometric.ids` `ContinuousLinearMap.instCompleteSpace` `IsBoundedSMul.continuousSMul` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeminormedAddCommGroup.to_isUniformAddGroup` `fderiv` `iteratedFDeriv_succ_apply_right`
`fderiv` 📖	mathematical	`HasFPowerSeriesOnBall`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv` `FormalMultilinearSeries.derivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `congr` `RingHomIsometric.ids` `smulCommClass_self` `RingHomInvPair.ids` `ContinuousLinearMap.comp_hasFPowerSeriesOnBall` `zero_add` `comp_sub` `mono` `FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin` `LT.lt.trans_le` `r_pos` `r_le` `fderiv_eq` `edist_eq_enorm_sub` `add_sub_cancel`
`fderiv_eq` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivAt.fderiv` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt`
`hasFDerivAt` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesAt.hasFDerivAt` `hasFPowerSeriesAt` `changeOrigin`
`hasSum_iteratedFDeriv` 📖	mathematical	`HasFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Nat.factorial` `DFunLike.coe` `ContinuousMultilinearMap` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `factorial_smul` `SMulCommClass.smul_comm` `AddMonoid.nat_smulCommClass'` `smul_assoc` `AddCommMonoid.nat_isScalarTower` `nsmul_eq_mul` `mul_inv_cancel₀` `Nat.cast_ne_zero` `Nat.factorial_ne_zero` `one_smul` `hasSum`
`iteratedFDeriv_zero_apply_diag` 📖	mathematical	`HasFPowerSeriesOnBall`	`iteratedFDeriv`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousMultilinearMap.ext` `coeff_zero`

HasFPowerSeriesWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableWithinAt` 📖	mathematical	`HasFPowerSeriesWithinAt`	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInsert`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivWithinAt.differentiableWithinAt` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `hasFDerivWithinAt`
`fderivWithin_eq` 📖	mathematical	`HasFPowerSeriesWithinAt` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInsert`	`fderivWithin` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivWithinAt.fderivWithin` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivWithinAt`
`hasFDerivWithinAt` 📖	mathematical	`HasFPowerSeriesWithinAt`	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `Set` `Set.instInsert`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `HasFDerivWithinAt.eq_1` `hasFDerivAtFilter_iff_isLittleO` `Asymptotics.isLittleO_iff` `nhdsWithin_prod_eq` `Filter.Tendsto.prodMk` `Filter.tendsto_id` `tendsto_const_nhdsWithin` `hasStrictFDerivWithinAt`
`hasStrictFDerivWithinAt` 📖	mathematical	`HasFPowerSeriesWithinAt`	`Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `nhdsWithin` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.instInsert` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `LinearIsometryEquiv` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Asymptotics.IsBigO.trans_isLittleO` `isBigO_image_sub_norm_mul_norm_sub` `Asymptotics.IsLittleO.of_norm_right` `Asymptotics.isLittleO_iff_exists_eq_mul` `Filter.Tendsto.mono_left` `Continuous.tendsto'` `Continuous.norm` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `Prod.instIsTopologicalAddGroup` `continuous_id` `continuous_const` `sub_self` `norm_zero` `nhdsWithin_le_nhds` `Filter.EventuallyEq.rfl`

HasFPowerSeriesWithinOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableOn` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInter` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `AnalyticWithinAt.differentiableWithinAt` `analyticWithinAt_of_mem` `eq_or_ne` `DifferentiableWithinAt.mono` `Set.inter_subset_left` `DifferentiableWithinAt.mono_of_mem_nhdsWithin` `Set.subset_insert` `nhdsWithin_insert_of_ne` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `self_mem_nhdsWithin` `nhdsWithin_mono`
`fderivWithin` 📖	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.instInsert`	`ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin` `FormalMultilinearSeries.derivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `congr'` `RingHomIsometric.ids` `smulCommClass_self` `RingHomInvPair.ids` `ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall` `HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall` `zero_add` `HasFPowerSeriesOnBall.comp_sub` `HasFPowerSeriesOnBall.mono` `FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin` `LT.lt.trans_le` `r_pos` `r_le` `fderivWithin_eq` `edist_eq_enorm_sub` `add_sub_cancel`
`fderivWithin_eq` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`fderivWithin` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivWithinAt.fderivWithin` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivWithinAt`
`fderivWithin_of_mem` 📖	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`	`ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin` `FormalMultilinearSeries.derivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `RingHomIsometric.ids` `smulCommClass_self` `fderivWithin`
`fderivWithin_of_mem_of_analyticOn` 📖	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`	`ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderivWithin` `FormalMultilinearSeries.derivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `smulCommClass_self` `LE.le.trans` `r_le` `FormalMultilinearSeries.radius_le_radius_derivSeries` `r_pos` `hasSum_derivSeries_of_hasFDerivWithinAt` `edist_zero_right` `Set.insert_eq_of_mem` `DifferentiableWithinAt.hasFDerivWithinAt` `AnalyticOn.differentiableOn`
`hasFDerivWithinAt` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `eq_or_ne` `add_zero` `HasFPowerSeriesWithinAt.hasFDerivWithinAt` `hasFPowerSeriesWithinAt` `changeOrigin` `HasFDerivWithinAt.mono_of_mem_nhdsWithin` `HasFDerivWithinAt.mono` `Set.subset_insert` `nhdsWithin_insert_of_ne` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `self_mem_nhdsWithin`
`hasSum_derivSeries_of_hasFDerivWithinAt` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup`	`HasSum` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.topologicalSpace` `DFunLike.coe` `ContinuousMultilinearMap` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `NormedSpace.toIsBoundedSMul` `ContinuousMultilinearMap.funLike` `FormalMultilinearSeries.derivSeries` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `RingHomIsometric.ids` `smulCommClass_self` `UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul` `UniformSpace.Completion.instUniformContinuousConstSMul` `RingHomCompTriple.ids` `Topology.IsInducing.hasSum_iff` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass` `Topology.IsEmbedding.toIsInducing` `LinearIsometry.isEmbedding` `ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall` `hasSum` `fderivWithin` `UniformSpace.Completion.completeSpace` `edist_zero_right` `HasFDerivWithinAt.fderivWithin` `IsBoundedSMul.continuousSMul` `UniformSpace.Completion.instIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivAt.comp_hasFDerivWithinAt` `ContinuousLinearMap.hasFDerivAt` `ContinuousLinearMap.ext` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `ContinuousMultilinearMap.sum_apply` `map_sum` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply`

HasFiniteFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableOn` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `AnalyticAt.differentiableWithinAt` `CPolynomialAt.analyticAt` `cpolynomialAt_of_mem`
`fderiv` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv` `FormalMultilinearSeries.derivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `congr` `RingHomIsometric.ids` `smulCommClass_self` `RingHomInvPair.ids` `ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall` `zero_add` `comp_sub` `mono` `FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin` `finite` `HasFPowerSeriesOnBall.r_pos` `toHasFPowerSeriesOnBall` `le_top` `fderiv_eq` `edist_eq_enorm_sub` `add_sub_cancel`
`fderiv'` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fderiv` `FormalMultilinearSeries.derivSeries`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `smulCommClass_self` `eq_or_ne` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `bound_zero_of_eq_zero` `Filter.EventuallyEq.fderiv_eq` `Filter.eventuallyEq_iff_exists_mem` `IsOpen.mem_nhds` `Metric.isOpen_eball` `eq_zero_of_bound_zero` `fderiv_fun_const` `HasFPowerSeriesOnBall.r_pos` `toHasFPowerSeriesOnBall` `ContinuousMultilinearMap.ext` `RingHomInvPair.ids` `FormalMultilinearSeries.changeOriginSeries_finite_of_finite` `finite` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `fderiv`
`fderiv_eq` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	`fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivAt.fderiv` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt`
`hasFDerivAt` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasStrictFDerivAt.hasFDerivAt` `RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `hasStrictFDerivAt`
`hasStrictFDerivAt` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `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` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `continuousMultilinearCurryFin1` `FormalMultilinearSeries.changeOrigin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesAt.hasStrictFDerivAt` `HasFPowerSeriesOnBall.hasFPowerSeriesAt` `toHasFPowerSeriesOnBall` `changeOrigin`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousMultilinearMap_apply` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `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` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace`	`DFunLike.coe` `ContinuousMultilinearMap.funLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `ContinuousLinearMap.comp` `ContinuousMultilinearMap.addCommMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `RingHomCompTriple.ids` `ContinuousMultilinearMap.apply` `IsBoundedSMul.continuousSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Finset.sum` `ContinuousLinearMap.addCommMonoid` `Finset.univ` `ContinuousMultilinearMap.toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.ext` `ContinuousLinearMap.coe_sum'` `Finset.sum_congr` `Finset.sum_apply` `ContinuousLinearMap.add_comp` `ContinuousMultilinearMap.linearDeriv_apply` `comp` `ContinuousMultilinearMap.hasStrictFDerivAt_uncurry` `prodMk` `hasStrictFDerivAt_pi` `Finite.of_fintype`

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt_symm` 📖	—	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AnalyticAt` `toFun'` `symm` `fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	—	`RingHomInvPair.ids` `right_inv` `analyticAt_symm'`
`analyticAt_symm'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AnalyticAt` `toFun'` `fderiv` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`symm`	—	`RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasFPowerSeriesAt.fderiv_eq` `LinearIsometryEquiv.symm_apply_apply` `HasFPowerSeriesAt.analyticAt` `hasFPowerSeriesAt_symm`

---

← Back to Index