Operations

📁 Source: Mathlib/Analysis/Calculus/ContDiff/Operations.lean

Statistics

Metric	Count
Definitions `restrContDiff`	1
Theorems `add`, `const_smul`, `div`, `div_const`, `fun_smul`, `inv`, `mul`, `neg`, `pow`, `prodMap`, `restrict_scalars`, `smul`, `smul_const`, `sub`, `sum`, `add`, `const_smul`, `div`, `div_const`, `fun_smul`, `inv`, `mul`, `neg`, `pow`, `prodMap`, `prodMap'`, `restrict_scalars`, `smul`, `smul_const`, `sub`, `sum`, `add`, `const_smul`, `div`, `div_const`, `fun_div`, `fun_smul`, `inv`, `mul`, `neg`, `pow`, `prodMap`, `restrict_scalars`, `smul`, `smul_const`, `sub`, `sum`, `add`, `const_smul`, `div`, `div_const`, `fun_smul`, `inv`, `mul`, `neg`, `pow`, `prodMap`, `prodMap'`, `restrict_scalars`, `smul`, `smul_const`, `sub`, `sum`, `contDiffAt_map_inverse`, `add`, `restrictScalars`, `contDiff_symm`, `contDiff_symm_deriv`, `contDiffAt_symm`, `contDiffAt_symm_deriv`, `contDiffOn_restrContDiff_source`, `contDiffOn_restrContDiff_target`, `restrContDiff_apply`, `restrContDiff_source`, `restrContDiff_symm_apply`, `restrContDiff_target`, `contDiffAt_apply`, `contDiffAt_inv`, `contDiffAt_map_inverse`, `contDiffAt_pi`, `contDiffAt_pi'`, `contDiffAt_prod`, `contDiffAt_prod'`, `contDiffAt_ringInverse`, `contDiffOn_apply`, `contDiffOn_inv`, `contDiffOn_pi`, `contDiffOn_pi'`, `contDiffOn_prod`, `contDiffOn_prod'`, `contDiffWithinAt_pi`, `contDiffWithinAt_prod`, `contDiffWithinAt_prod'`, `contDiff_add`, `contDiff_apply`, `contDiff_apply_apply`, `contDiff_const_smul`, `contDiff_mul`, `contDiff_neg`, `contDiff_pi`, `contDiff_pi'`, `contDiff_prod`, `contDiff_prod'`, `contDiff_prodMk_left`, `contDiff_prodMk_right`, `contDiff_single`, `contDiff_smul`, `contDiff_smul_const`, `contDiff_update`, `hasFTaylorSeriesUpToOn_pi`, `hasFTaylorSeriesUpToOn_pi'`, `iteratedFDerivWithin_add_apply`, `iteratedFDerivWithin_add_apply'`, `iteratedFDerivWithin_const_smul_apply`, `iteratedFDerivWithin_neg_apply`, `iteratedFDerivWithin_smul_const_apply`, `iteratedFDerivWithin_sum_apply`, `iteratedFDeriv_add`, `iteratedFDeriv_add_apply`, `iteratedFDeriv_add_apply'`, `iteratedFDeriv_const_smul_apply`, `iteratedFDeriv_const_smul_apply'`, `iteratedFDeriv_neg`, `iteratedFDeriv_neg_apply`, `iteratedFDeriv_smul_const_apply`, `iteratedFDeriv_sum`	126
Total	127

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContDiff`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `contDiff_add` `prodMk`
`const_smul` 📖	mathematical	`ContDiff`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass`	—	`comp` `contDiff_const_smul`
`div` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`ContDiffAt.div`
`div_const` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div_eq_mul_inv` `mul` `contDiff_const`
`fun_smul` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`smul`
`inv` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`contDiff_iff_contDiffAt` `ContDiffAt.inv` `contDiffAt`
`mul` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`comp` `contDiff_mul` `prodMk`
`neg` 📖	mathematical	`ContDiff`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `contDiff_neg`
`pow` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`pow_zero` `contDiff_const` `pow_succ` `mul`
`prodMap` 📖	mathematical	`ContDiff`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiff_iff_contDiffAt` `ContDiffAt.prodMap`
`restrict_scalars` 📖	—	`ContDiff`	—	—	`contDiff_iff_contDiffAt` `ContDiffAt.restrict_scalars` `contDiffAt`
`smul` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `contDiff_smul` `prodMk`
`smul_const` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `contDiff_smul_const`
`sub` 📖	mathematical	`ContDiff`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`sum` 📖	mathematical	`ContDiff`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffOn.sum`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContDiffAt`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.add`
`const_smul` 📖	mathematical	`ContDiffAt`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.const_smul`
`div` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`ContDiffWithinAt.div`
`div_const` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`ContDiffWithinAt.div_const`
`fun_smul` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`smul`
`inv` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`ContDiffWithinAt.inv`
`mul` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`ContDiffWithinAt.mul`
`neg` 📖	mathematical	`ContDiffAt`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.neg`
`pow` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`ContDiffWithinAt.pow`
`prodMap` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`eq_1` `Set.univ_prod_univ` `ContDiffWithinAt.prodMap`
`prodMap'` 📖	mathematical	`ContDiffAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`prodMap`
`restrict_scalars` 📖	—	`ContDiffAt`	—	—	`contDiffWithinAt_univ` `ContDiffWithinAt.restrict_scalars` `contDiffWithinAt`
`smul` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.smul`
`smul_const` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.smul_const`
`sub` 📖	mathematical	`ContDiffAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`sum` 📖	mathematical	`ContDiffAt`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`contDiffWithinAt_univ` `ContDiffWithinAt.sum`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContDiffOn`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffWithinAt.add`
`const_smul` 📖	mathematical	`ContDiffOn`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass`	—	`ContDiffWithinAt.const_smul`
`div` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`ContDiffWithinAt.div`
`div_const` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`ContDiffWithinAt.div_const`
`fun_div` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div`
`fun_smul` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`smul`
`inv` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`ContDiffWithinAt.inv` `contDiffWithinAt`
`mul` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`ContDiffWithinAt.mul`
`neg` 📖	mathematical	`ContDiffOn`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffWithinAt.neg`
`pow` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`ContDiffWithinAt.pow`
`prodMap` 📖	mathematical	`ContDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `contDiffOn_fst` `Set.prod_subset_preimage_fst` `contDiffOn_snd` `Set.prod_subset_preimage_snd`
`restrict_scalars` 📖	—	`ContDiffOn`	—	—	`ContDiffWithinAt.restrict_scalars`
`smul` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffWithinAt.smul`
`smul_const` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffWithinAt.smul_const`
`sub` 📖	mathematical	`ContDiffOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`sum` 📖	mathematical	`ContDiffOn`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffWithinAt.sum`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContDiffWithinAt`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `ContDiff.contDiffWithinAt` `contDiff_add` `prodMk` `Set.subset_preimage_univ`
`const_smul` 📖	mathematical	`ContDiffWithinAt`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass`	—	`ContDiffAt.comp_contDiffWithinAt` `ContDiff.contDiffAt` `contDiff_const_smul`
`div` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div_eq_mul_inv` `mul` `inv`
`div_const` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`div_eq_mul_inv` `mul` `contDiffWithinAt_const`
`fun_smul` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`smul`
`inv` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`ContDiffAt.comp_contDiffWithinAt` `contDiffAt_inv`
`mul` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`ContDiff.comp_contDiffWithinAt` `contDiff_mul` `prodMk`
`neg` 📖	mathematical	`ContDiffWithinAt`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `ContDiff.contDiffWithinAt` `contDiff_neg` `Set.subset_preimage_univ`
`pow` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`ContDiff.comp_contDiffWithinAt` `ContDiff.pow` `contDiff_id`
`prodMap` 📖	mathematical	`ContDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMap'`
`prodMap'` 📖	mathematical	`ContDiffWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `contDiffWithinAt_fst` `Set.prod_subset_preimage_fst` `contDiffWithinAt_snd` `Set.prod_subset_preimage_snd`
`restrict_scalars` 📖	—	`ContDiffWithinAt`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFTaylorSeriesUpToOn.restrictScalars` `AnalyticOnNhd.comp_analyticOn` `IsScalarTower.to_smulCommClass'` `smulCommClass_self` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.analyticOnNhd` `AnalyticOn.restrictScalars` `ContinuousMultilinearMap.instIsScalarTower` `Set.mapsTo_univ`
`smul` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`comp` `ContDiff.contDiffWithinAt` `contDiff_smul` `prodMk` `Set.subset_preimage_univ`
`smul_const` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContDiffAt.comp_contDiffWithinAt` `ContDiff.contDiffAt` `contDiff_smul_const`
`sub` 📖	mathematical	`ContDiffWithinAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`sum` 📖	mathematical	`ContDiffWithinAt`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Finset.induction_on` `Finset.sum_insert` `add` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`

ContinuousLinearMap.IsInvertible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_map_inverse` 📖	mathematical	`ContinuousLinearMap.IsInvertible` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	`ContDiffAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.inverse`	—	`RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `contDiffAt_map_inverse`

HasFTaylorSeriesUpToOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`HasFTaylorSeriesUpToOn`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `FormalMultilinearSeries` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `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` `NormedSpace.toIsBoundedSMul` `FormalMultilinearSeries.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `continuousLinearMap_comp` `prodMk`
`restrictScalars` 📖	mathematical	`HasFTaylorSeriesUpToOn`	`FormalMultilinearSeries.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `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` `NormedSpace.toIsBoundedSMul` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `zero_eq` `HasFDerivAt.comp_hasFDerivWithinAt` `IsScalarTower.to_smulCommClass'` `smulCommClass_self` `LinearMap.IsScalarTower.compatibleSMul` `ContinuousMultilinearMap.instIsScalarTower` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsBoundedSMul.continuousSMul` `ContinuousLinearMap.hasFDerivAt` `HasFDerivWithinAt.restrictScalars` `fderivWithin` `Continuous.comp_continuousOn` `ContinuousMultilinearMap.continuous_restrictScalars` `cont`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_symm` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContDiff`	`symm`	—	`RingHomInvPair.ids` `contDiff_iff_contDiffAt` `OpenPartialHomeomorph.contDiffAt_symm` `Set.mem_univ` `ContDiff.contDiffAt`
`contDiff_symm_deriv` 📖	mathematical	`HasDerivAt` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `ContinuousMul.to_continuousSMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `ContDiff`	`symm`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `contDiff_iff_contDiffAt` `OpenPartialHomeomorph.contDiffAt_symm_deriv` `Set.mem_univ` `ContDiff.contDiffAt`

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
`restrContDiff` 📖	CompOp	6 math math: `restrContDiff_target`, `restrContDiff_symm_apply`, `restrContDiff_source`, `contDiffOn_restrContDiff_source`, `contDiffOn_restrContDiff_target`, `restrContDiff_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_symm` 📖	—	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `toFun'` `ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `symm` `ContDiffAt`	—	—	`RingHomInvPair.ids` `AnalyticAt.contDiffAt` `analyticAt_symm` `ContDiffAt.analyticAt` `HasFDerivAt.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ENat.nat_induction` `contDiffAt_zero` `IsOpen.mem_nhds` `open_target` `continuousOn_invFun` `RingHomIsometric.ids` `smulCommClass_self` `contDiffAt_succ_iff_hasFDerivAt` `HasFDerivAt.unique` `mem_of_mem_nhds` `ContinuousLinearEquiv.nhds` `ContinuousAt.preimage_mem_nhds` `ContDiffAt.continuousAt` `mem_nhds_iff` `Filter.inter_mem` `isOpen_inter_preimage_symm` `Set.mem_inter` `Set.mem_preimage` `ContinuousLinearMap.inverse_equiv` `hasFDerivAt_symm` `contDiffAt_map_inverse` `ContDiffAt.of_le` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ContDiffAt.comp` `contDiffAt_infty`
`contDiffAt_symm_deriv` 📖	—	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `HasDerivAt` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousMul.to_continuousSMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `toFun'` `symm` `ContDiffAt`	—	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `contDiffAt_symm` `RingHomInvPair.ids` `HasDerivAt.hasFDerivAt_equiv`
`contDiffOn_restrContDiff_source` 📖	mathematical	—	`ContDiffOn` `toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.source` `toPartialEquiv` `restrContDiff`	—	`ContDiffAt.contDiffWithinAt`
`contDiffOn_restrContDiff_target` 📖	mathematical	—	`ContDiffOn` `toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `symm` `PartialEquiv.target` `toPartialEquiv` `restrContDiff`	—	`ContDiffAt.contDiffWithinAt`
`restrContDiff_apply` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `restrContDiff`	—	—
`restrContDiff_source` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `restrContDiff` `Set` `Set.instInter` `setOf` `ContDiffAt` `toFun'` `symm`	—	—
`restrContDiff_symm_apply` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `symm` `restrContDiff`	—	—
`restrContDiff_target` 📖	mathematical	—	`PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `restrContDiff` `Set` `Set.instInter` `setOf` `ContDiffAt` `toFun'` `symm`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt_apply` 📖	mathematical	—	`ContDiffAt` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffAt` `contDiff_apply`
`contDiffAt_inv` 📖	mathematical	—	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField`	—	`Ring.inverse_eq_inv'` `contDiffAt_ringInverse` `instHasSummableGeomSeries`
`contDiffAt_map_inverse` 📖	mathematical	—	`ContDiffAt` `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` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.inverse` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `RingHomIsometric.ids` `smulCommClass_self` `Unique.instSubsingleton` `RingHomCompTriple.ids` `ContinuousLinearMap.inverse_eq_ringInverse` `ContDiff.clm_comp` `contDiff_id` `contDiff_const` `ContDiffAt.comp` `ContDiff.contDiffAt` `ContinuousLinearEquiv.coe_symm_comp_coe` `contDiffAt_ringInverse` `instHasSummableGeomSeriesOfCompleteSpace` `ContinuousLinearMap.instCompleteSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeminormedAddCommGroup.to_isUniformAddGroup`
`contDiffAt_pi` 📖	mathematical	—	`ContDiffAt` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffWithinAt_pi`
`contDiffAt_pi'` 📖	mathematical	`ContDiffAt`	`Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffAt_pi`
`contDiffAt_prod` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiffWithinAt_prod`
`contDiffAt_prod'` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiffWithinAt_prod'`
`contDiffAt_ringInverse` 📖	mathematical	—	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Units.val` `MonoidWithZero.toMonoid`	—	`AnalyticOnNhd.contDiffOn` `analyticOnNhd_inverse` `IsOpen.uniqueDiffOn` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Units.isOpen` `Units.isUnit` `ContDiffWithinAt.contDiffAt` `IsOpen.mem_nhds`
`contDiffOn_apply` 📖	mathematical	—	`ContDiffOn` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.contDiffOn` `contDiff_apply`
`contDiffOn_inv` 📖	mathematical	—	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`ContDiffAt.contDiffWithinAt` `contDiffAt_inv`
`contDiffOn_pi` 📖	mathematical	—	`ContDiffOn` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffWithinAt_pi`
`contDiffOn_pi'` 📖	mathematical	`ContDiffOn`	`Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiffOn_pi`
`contDiffOn_prod` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiffWithinAt_prod`
`contDiffOn_prod'` 📖	mathematical	`ContDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiffWithinAt_prod'`
`contDiffWithinAt_pi` 📖	mathematical	—	`ContDiffWithinAt` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiffWithinAt.continuousLinearMap_comp` `Filter.iInter_mem` `Finite.of_fintype` `hasFTaylorSeriesUpToOn_pi` `HasFTaylorSeriesUpToOn.mono` `Set.iInter_subset` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `instContinuousConstSMulForall` `Pi.smulCommClass` `AnalyticOnNhd.comp_analyticOn` `LinearIsometryEquiv.analyticOnNhd` `AnalyticOn.pi` `AnalyticOn.mono` `Set.mapsTo_univ`
`contDiffWithinAt_prod` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiffWithinAt_prod'`
`contDiffWithinAt_prod'` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`Finset.prod_induction` `ContDiffWithinAt.mul` `contDiffWithinAt_const`
`contDiff_add` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsBoundedLinearMap.contDiff` `IsBoundedLinearMap.add` `IsBoundedLinearMap.fst` `IsBoundedLinearMap.snd`
`contDiff_apply` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiff_pi` `contDiff_id`
`contDiff_apply_apply` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `Pi.seminormedAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiff_pi` `contDiff_apply`
`contDiff_const_smul` 📖	mathematical	—	`ContDiff` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass`	—	`ContinuousLinearMap.contDiff`
`contDiff_mul` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAlgebra.toNormedSpace` `NormedRing.toSeminormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`IsBoundedBilinearMap.contDiff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.right` `Algebra.to_smulCommClass` `ContinuousLinearMap.isBoundedBilinearMap`
`contDiff_neg` 📖	mathematical	—	`ContDiff` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsBoundedLinearMap.contDiff` `IsBoundedLinearMap.neg` `IsBoundedLinearMap.id`
`contDiff_pi` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—
`contDiff_pi'` 📖	mathematical	`ContDiff`	`Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`contDiff_pi`
`contDiff_prod` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiff_iff_contDiffAt` `contDiffAt_prod` `ContDiff.contDiffAt`
`contDiff_prod'` 📖	mathematical	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`contDiff_iff_contDiffAt` `contDiffAt_prod'` `ContDiff.contDiffAt`
`contDiff_prodMk_left` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.prodMk` `contDiff_id` `contDiff_const`
`contDiff_prodMk_right` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContDiff.prodMk` `contDiff_const` `contDiff_id`
`contDiff_single` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`contDiff_update`
`contDiff_smul` 📖	mathematical	—	`ContDiff` `Prod.normedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAlgebra.toNormedSpace` `NormedRing.toSeminormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsBoundedBilinearMap.contDiff` `isBoundedBilinearMap_smul`
`contDiff_smul_const` 📖	mathematical	—	`ContDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`ContinuousLinearMap.contDiff` `IsBoundedSMul.continuousSMul`
`contDiff_update` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Function.update`	—	`contDiff_pi` `contDiff_id` `contDiff_const`
`hasFTaylorSeriesUpToOn_pi` 📖	mathematical	—	`HasFTaylorSeriesUpToOn` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMultilinearMap.pi` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `smulCommClass_self` `instContinuousConstSMulForall` `Pi.smulCommClass` `HasFTaylorSeriesUpToOn.continuousLinearMap_comp` `HasFTaylorSeriesUpToOn.zero_eq` `HasFDerivAt.comp_hasFDerivWithinAt` `LinearIsometryEquiv.hasFDerivAt` `hasFDerivWithinAt_pi` `Finite.of_fintype` `HasFTaylorSeriesUpToOn.fderivWithin` `Continuous.comp_continuousOn` `LinearIsometryEquiv.continuous` `continuousOn_pi` `HasFTaylorSeriesUpToOn.cont`
`hasFTaylorSeriesUpToOn_pi'` 📖	mathematical	—	`HasFTaylorSeriesUpToOn` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap.compContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Pi.module` `Pi.topologicalSpace` `ContinuousLinearMap.proj`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Pi.continuousAdd` `instContinuousConstSMulForall` `ContinuousMultilinearMap.ext` `hasFTaylorSeriesUpToOn_pi`
`iteratedFDerivWithin_add_apply` 📖	mathematical	`ContDiffWithinAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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`	`iteratedFDerivWithin` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`Filter.Eventually.and` `ContDiffWithinAt.eventually` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `mem_nhdsWithin` `ContDiffWithinAt.mono` `Set.insert_eq_of_mem` `Set.inter_subset_left` `UniqueDiffOn.inter` `Filter.inter_eventuallyEq_left` `Filter.eventually_of_mem` `IsOpen.mem_nhds` `iteratedFDerivWithin_congr_set` `HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFTaylorSeriesUpToOn.add` `ContDiffOn.ftaylorSeriesWithin` `le_rfl`
`iteratedFDerivWithin_add_apply'` 📖	mathematical	`ContDiffWithinAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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`	`iteratedFDerivWithin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`iteratedFDerivWithin_add_apply`
`iteratedFDerivWithin_const_smul_apply` 📖	mathematical	`ContDiffWithinAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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`	`iteratedFDerivWithin` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ContinuousMultilinearMap.instSMul`	—	`ContinuousLinearMap.iteratedFDerivWithin_comp_left` `le_rfl`
`iteratedFDerivWithin_neg_apply` 📖	mathematical	`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`	`iteratedFDerivWithin` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.instNeg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.ext` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `iteratedFDerivWithin_succ_apply_left` `fderivWithin_congr'` `Pi.neg_def` `fderivWithin_neg` `ContinuousLinearMap.neg_apply` `ContinuousMultilinearMap.neg_apply`
`iteratedFDerivWithin_smul_const_apply` 📖	mathematical	`ContDiffWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`iteratedFDerivWithin` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.compContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `SeminormedRing.toPseudoMetricSpace` `ContinuousLinearMap.smulRight` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommMonoid.toAddMonoid` `ContinuousLinearMap.id`	—	`ContinuousLinearMap.iteratedFDerivWithin_comp_left` `IsBoundedSMul.continuousSMul` `le_rfl`
`iteratedFDerivWithin_sum_apply` 📖	mathematical	`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` `ContDiffWithinAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDerivWithin` `Finset.sum` `AddCommGroup.toAddCommMonoid` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype`	—	`Finset.cons_induction` `iteratedFDerivWithin_zero_fun` `Finset.sum_cons` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin_add_apply'` `ContDiffWithinAt.sum`
`iteratedFDeriv_add` 📖	mathematical	`ContDiff` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `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.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDeriv_add_apply` `ContDiff.contDiffAt`
`iteratedFDeriv_add_apply` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `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.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin_add_apply` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`iteratedFDeriv_add_apply'` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `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.instAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`iteratedFDeriv_add_apply`
`iteratedFDeriv_const_smul_apply` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instSMul`	—	`ContinuousLinearMap.iteratedFDeriv_comp_left` `le_rfl`
`iteratedFDeriv_const_smul_apply'` 📖	mathematical	`ContDiffAt` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instSMul`	—	`iteratedFDeriv_const_smul_apply`
`iteratedFDeriv_neg` 📖	mathematical	—	`iteratedFDeriv` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `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.instNeg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDeriv_neg_apply`
`iteratedFDeriv_neg_apply` 📖	mathematical	—	`iteratedFDeriv` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `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.instNeg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin_neg_apply` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ`
`iteratedFDeriv_smul_const_apply` 📖	mathematical	`ContDiffAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.compContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `SeminormedRing.toPseudoMetricSpace` `ContinuousLinearMap.smulRight` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommMonoid.toAddMonoid` `ContinuousLinearMap.id`	—	`ContinuousLinearMap.iteratedFDeriv_comp_left` `IsBoundedSMul.continuousSMul` `le_rfl`
`iteratedFDeriv_sum` 📖	mathematical	`ContDiff` `WithTop` `ENat` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`iteratedFDeriv` `Finset.sum` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Pi.addCommGroup` `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`	—	`Finset.sum_apply` `iteratedFDerivWithin_univ` `Finset.sum_congr` `iteratedFDerivWithin_sum_apply` `uniqueDiffOn_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.mem_univ` `ContDiff.contDiffWithinAt`

---

← Back to Index