SpecificFunctions

📁 Source: Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

Statistics

Metric	Count
Definitions	0
Theorems `hasMFDerivAt`, `hasMFDerivWithinAt`, `mdifferentiable`, `mdifferentiableAt`, `mdifferentiableOn`, `mdifferentiableWithinAt`, `mfderivWithin_eq`, `mfderiv_eq`, `hasMFDerivAt`, `hasMFDerivWithinAt`, `mdifferentiable`, `mdifferentiableAt`, `mdifferentiableOn`, `mdifferentiableWithinAt`, `mfderivWithin_eq`, `mfderiv_eq`, `add`, `const_smul`, `mul`, `mul'`, `neg`, `prod`, `prodMap`, `prodMk`, `sub`, `sum`, `add`, `mul`, `mul'`, `neg`, `prod`, `prodMap`, `prodMk`, `sum`, `add`, `const_smul`, `fst`, `mul`, `neg`, `pow`, `prod`, `prodMap`, `prodMk`, `prodMk_space`, `snd`, `sub`, `sum`, `add`, `const_smul`, `fst`, `mfderiv_prod`, `mul`, `neg`, `pow`, `prod`, `prodMap`, `prodMap'`, `prodMk`, `prodMk_space`, `snd`, `sub`, `sum`, `add`, `mul`, `neg`, `pow`, `prod`, `prodMap`, `prodMk`, `prodMk_space`, `sum`, `add`, `fst`, `mul`, `neg`, `pow`, `prod`, `prodMap`, `prodMap'`, `prodMk`, `prodMk_space`, `snd`, `sum`, `const_smul_mfderiv`, `hasMFDerivAt_const`, `hasMFDerivAt_fst`, `hasMFDerivAt_id`, `hasMFDerivAt_inl`, `hasMFDerivAt_inr`, `hasMFDerivAt_neg`, `hasMFDerivAt_snd`, `hasMFDerivAt_sumSwap`, `hasMFDerivWithinAt_const`, `hasMFDerivWithinAt_fst`, `hasMFDerivWithinAt_id`, `hasMFDerivWithinAt_inl`, `hasMFDerivWithinAt_inr`, `hasMFDerivWithinAt_snd`, `mdifferentiableAt_const`, `mdifferentiableAt_fst`, `mdifferentiableAt_id`, `mdifferentiableAt_neg`, `mdifferentiableAt_prod_iff`, `mdifferentiableAt_prod_module_iff`, `mdifferentiableAt_snd`, `mdifferentiableOn_const`, `mdifferentiableOn_fst`, `mdifferentiableOn_id`, `mdifferentiableOn_prod_iff`, `mdifferentiableOn_prod_module_iff`, `mdifferentiableOn_snd`, `mdifferentiableWithinAt_const`, `mdifferentiableWithinAt_fst`, `mdifferentiableWithinAt_id`, `mdifferentiableWithinAt_prod_iff`, `mdifferentiableWithinAt_prod_module_iff`, `mdifferentiableWithinAt_snd`, `mdifferentiable_const`, `mdifferentiable_fst`, `mdifferentiable_id`, `mdifferentiable_prod_iff`, `mdifferentiable_prod_module_iff`, `mdifferentiable_snd`, `mfderivWithin_const`, `mfderivWithin_fst`, `mfderivWithin_id`, `mfderivWithin_prodMap`, `mfderivWithin_prodMk`, `mfderivWithin_snd`, `mfderivWithin_sumInl`, `mfderivWithin_sumInr`, `mfderivWithin_sumSwap`, `mfderiv_add`, `mfderiv_const`, `mfderiv_fst`, `mfderiv_id`, `mfderiv_neg`, `mfderiv_prodMap`, `mfderiv_prodMk`, `mfderiv_prod_eq_add`, `mfderiv_prod_eq_add_apply`, `mfderiv_prod_eq_add_comp`, `mfderiv_prod_left`, `mfderiv_prod_right`, `mfderiv_snd`, `mfderiv_sub`, `mfderiv_sumInl`, `mfderiv_sumInr`, `mfderiv_sumSwap`, `tangentMapWithin_id`, `tangentMapWithin_prodFst`, `tangentMapWithin_prodSnd`, `tangentMap_id`, `tangentMap_prodFst`, `tangentMap_prodSnd`, `tangentMap_prod_left`, `tangentMap_prod_right`, `writtenInExtChartAt_sumInl_eventuallyEq_id`, `writtenInExtChartAt_sumInr_eventuallyEq_id`, `writtenInExtChartAt_sumSwap_eventuallyEq_id`	160
Total	160

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMFDerivAt` 📖	mathematical	—	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `HasFDerivAt.hasMFDerivAt` `hasFDerivAt`
`hasMFDerivWithinAt` 📖	mathematical	—	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `HasFDerivWithinAt.hasMFDerivWithinAt` `hasFDerivWithinAt`
`mdifferentiable` 📖	mathematical	—	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `Differentiable.mdifferentiable` `differentiable`
`mdifferentiableAt` 📖	mathematical	—	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `DifferentiableAt.mdifferentiableAt` `differentiableAt`
`mdifferentiableOn` 📖	mathematical	—	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `DifferentiableOn.mdifferentiableOn` `differentiableOn`
`mdifferentiableWithinAt` 📖	mathematical	—	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `DifferentiableWithinAt.mdifferentiableWithinAt` `differentiableWithinAt`
`mfderivWithin_eq` 📖	mathematical	`UniqueMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`mfderivWithin` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `HasMFDerivWithinAt.mfderivWithin` `hasMFDerivWithinAt`
`mfderiv_eq` 📖	mathematical	—	`mfderiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `HasMFDerivAt.mfderiv` `hasMFDerivAt`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMFDerivAt` 📖	mathematical	—	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`HasFDerivAt.hasMFDerivAt` `hasFDerivAt`
`hasMFDerivWithinAt` 📖	mathematical	—	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`HasFDerivWithinAt.hasMFDerivWithinAt` `hasFDerivWithinAt`
`mdifferentiable` 📖	mathematical	—	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`Differentiable.mdifferentiable` `differentiable`
`mdifferentiableAt` 📖	mathematical	—	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`DifferentiableAt.mdifferentiableAt` `differentiableAt`
`mdifferentiableOn` 📖	mathematical	—	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`DifferentiableOn.mdifferentiableOn` `differentiableOn`
`mdifferentiableWithinAt` 📖	mathematical	—	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`DifferentiableWithinAt.mdifferentiableWithinAt` `differentiableWithinAt`
`mfderivWithin_eq` 📖	mathematical	`UniqueMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`mfderivWithin` `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` `funLike`	—	`HasMFDerivWithinAt.mfderivWithin` `hasMFDerivWithinAt`
`mfderiv_eq` 📖	mathematical	—	`mfderiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `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` `funLike`	—	`HasMFDerivAt.mfderiv` `hasMFDerivAt`

HasMFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.add` `HasFDerivWithinAt.add`
`const_smul` 📖	mathematical	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `ContinuousLinearMap.instSMul` `AddCommMonoid.toAddMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul`	—	`smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousAt.const_smul` `HasFDerivWithinAt.const_smul`
`mul` 📖	mathematical	`HasMFDerivAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `hasMFDerivWithinAt_univ` `HasMFDerivWithinAt.mul` `hasMFDerivWithinAt`
`mul'` 📖	mathematical	`HasMFDerivAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ContinuousLinearMap.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `MulOpposite` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulOpposite.instSemiring` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `MulOpposite.op`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.opposite_mid` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `hasMFDerivWithinAt_univ` `HasMFDerivWithinAt.mul'` `hasMFDerivWithinAt`
`neg` 📖	mathematical	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.neg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `instAddCommGroupTangentSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.neg` `IsTopologicalAddGroup.toContinuousNeg` `HasFDerivWithinAt.neg`
`prod` 📖	mathematical	`HasMFDerivAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Finset.erase`	—	`IsTopologicalAddGroup.toContinuousAdd` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `HasMFDerivWithinAt.prod`
`prodMap` 📖	mathematical	`HasMFDerivAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prodMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.toModule` `mfderiv`	—	`mfderivWithin_univ` `mfderiv` `HasMFDerivWithinAt.prodMap` `hasMFDerivWithinAt`
`prodMk` 📖	mathematical	`HasMFDerivAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.toModule`	—	`ContinuousAt.prodMk` `HasFDerivWithinAt.prodMk`
`sub` 📖	mathematical	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.sub` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `instAddCommGroupTangentSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `HasFDerivWithinAt.sub`
`sum` 📖	mathematical	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `HasMFDerivWithinAt.sum`

HasMFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousWithinAt.add` `HasFDerivWithinAt.add`
`mul` 📖	mathematical	`HasMFDerivWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.opposite_mid` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `ContinuousLinearMap.ext` `mul_comm` `mul'`
`mul'` 📖	mathematical	`HasMFDerivWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ContinuousLinearMap.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `MulOpposite` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulOpposite.instSemiring` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `MulOpposite.op`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.opposite_mid` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `ContinuousWithinAt.mul` `PartialEquiv.trans_refl` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `HasFDerivWithinAt.mul'`
`neg` 📖	mathematical	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.neg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `instAddCommGroupTangentSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousWithinAt.neg` `IsTopologicalAddGroup.toContinuousNeg` `HasFDerivWithinAt.neg`
`prod` 📖	mathematical	`HasMFDerivWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Finset.erase`	—	`Finset.induction_on` `IsTopologicalAddGroup.toContinuousAdd` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Finset.sum_congr` `Finset.prod_congr` `Finset.erase_eq_of_notMem` `one_smul` `hasMFDerivWithinAt_const` `Finset.sum_insert` `Finset.erase_insert` `Finset.prod_insert` `add_comm` `IsTopologicalSemiring.toContinuousAdd` `Finset.smul_sum` `Finset.erase_insert_of_ne` `Finset.prod_apply` `mul` `Finset.forall_mem_insert`
`prodMap` 📖	mathematical	`HasMFDerivWithinAt` `Set.image`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prodMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.toModule`	—	`ContinuousWithinAt.mono` `ContinuousWithinAt.prodMap` `Set.range_prodMap` `PartialEquiv.prod_symm` `writtenInExtChart_prod` `HasFDerivWithinAt.mono` `HasFDerivWithinAt.prodMap` `Set.fst_image_prod_subset` `Set.snd_image_prod_subset`
`prodMk` 📖	mathematical	`HasMFDerivWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.toModule`	—	`ContinuousWithinAt.prodMk` `HasFDerivWithinAt.prodMk`
`sum` 📖	mathematical	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace`	—	`Finset.induction_on` `IsTopologicalAddGroup.toContinuousAdd` `hasMFDerivWithinAt_const`

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MDifferentiableAt.add`
`const_smul` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`MDifferentiableAt.const_smul`
`fst` 📖	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `mdifferentiable_fst`
`mul` 📖	mathematical	`MDifferentiable` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`MDifferentiableAt.mul`
`neg` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MDifferentiableAt.neg`
`pow` 📖	mathematical	`MDifferentiable` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`MDifferentiableAt.pow`
`prod` 📖	mathematical	`MDifferentiable` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`MDifferentiableAt.prod`
`prodMap` 📖	mathematical	`MDifferentiable`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiableAt.prodMap'`
`prodMk` 📖	mathematical	`MDifferentiable`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiableAt.prodMk`
`prodMk_space` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`MDifferentiableAt.prodMk_space`
`snd` 📖	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `mdifferentiable_snd`
`sub` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`MDifferentiableAt.sub`
`sum` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MDifferentiableAt.sum`

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HasMFDerivAt.mdifferentiableAt` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivAt.add` `hasMFDerivAt`
`const_smul` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`HasMFDerivAt.mdifferentiableAt` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasMFDerivAt.const_smul` `hasMFDerivAt`
`fst` 📖	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `mdifferentiableAt_fst`
`mfderiv_prod` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`mfderiv_prodMk`
`mul` 📖	mathematical	`MDifferentiableAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`HasMFDerivAt.mdifferentiableAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.opposite_mid` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `HasMFDerivAt.mul'` `hasMFDerivAt`
`neg` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`HasMFDerivAt.mdifferentiableAt` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivAt.neg` `hasMFDerivAt`
`pow` 📖	mathematical	`MDifferentiableAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`mdifferentiableWithinAt_univ` `MDifferentiableWithinAt.pow` `mdifferentiableWithinAt`
`prod` 📖	mathematical	`MDifferentiableAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`MDifferentiableWithinAt.prod`
`prodMap` 📖	mathematical	`MDifferentiableAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`mdifferentiableWithinAt_univ` `Set.univ_prod_univ` `MDifferentiableWithinAt.prodMap`
`prodMap'` 📖	mathematical	`MDifferentiableAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`prodMap`
`prodMk` 📖	mathematical	`MDifferentiableAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContinuousWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `DifferentiableWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.prop`
`prodMk_space` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`ContinuousWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `DifferentiableWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.prop`
`snd` 📖	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`comp` `mdifferentiableAt_snd`
`sub` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`HasMFDerivAt.mdifferentiableAt` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivAt.sub` `hasMFDerivAt`
`sum` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MDifferentiableWithinAt.sum`

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MDifferentiableWithinAt.add`
`mul` 📖	mathematical	`MDifferentiableOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`MDifferentiableWithinAt.mul`
`neg` 📖	mathematical	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MDifferentiableWithinAt.neg`
`pow` 📖	mathematical	`MDifferentiableOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`MDifferentiableWithinAt.pow`
`prod` 📖	mathematical	`MDifferentiableOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`MDifferentiableWithinAt.prod`
`prodMap` 📖	mathematical	`MDifferentiableOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `mdifferentiableOn_fst` `Set.prod_subset_preimage_fst` `mdifferentiableOn_snd` `Set.prod_subset_preimage_snd`
`prodMk` 📖	mathematical	`MDifferentiableOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiableWithinAt.prodMk`
`prodMk_space` 📖	mathematical	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`MDifferentiableWithinAt.prodMk_space`
`sum` 📖	mathematical	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MDifferentiableWithinAt.sum`

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivWithinAt.add` `hasMFDerivWithinAt`
`fst` 📖	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`MDifferentiableAt.comp_mdifferentiableWithinAt` `mdifferentiableAt_fst`
`mul` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.opposite_mid` `IsScalarTower.right` `Ring.uniformContinuousConstSMul_op` `HasMFDerivWithinAt.mul'` `hasMFDerivWithinAt`
`neg` 📖	mathematical	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivWithinAt.neg` `hasMFDerivWithinAt`
`pow` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`pow_zero` `mdifferentiableWithinAt_const` `pow_succ` `mul`
`prod` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf`	`Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `NormedCommRing.toCommRing`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `HasMFDerivWithinAt.prod` `hasMFDerivWithinAt`
`prodMap` 📖	mathematical	`MDifferentiableWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMap'`
`prodMap'` 📖	mathematical	`MDifferentiableWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `mdifferentiableWithinAt_fst` `Set.prod_subset_preimage_fst` `mdifferentiableWithinAt_snd` `Set.prod_subset_preimage_snd`
`prodMk` 📖	mathematical	`MDifferentiableWithinAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContinuousWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `DifferentiableWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.prop`
`prodMk_space` 📖	mathematical	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceProd`	—	`ContinuousWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.continuousWithinAt` `DifferentiableWithinAt.prodMk` `ChartedSpace.LiftPropWithinAt.prop`
`snd` 📖	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	—	`MDifferentiableAt.comp_mdifferentiableWithinAt` `mdifferentiableAt_snd`
`sum` 📖	mathematical	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `HasMFDerivWithinAt.sum` `hasMFDerivWithinAt`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul_mfderiv` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`mfderiv` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `ContinuousLinearMap.instSMul` `AddCommMonoid.toAddMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `instContinuousConstSMulTangentSpace`	—	`HasMFDerivAt.mfderiv` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasMFDerivAt.const_smul` `MDifferentiableAt.hasMFDerivAt`
`hasMFDerivAt_const` 📖	mathematical	—	`HasMFDerivAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	`continuousAt_const`
`hasMFDerivAt_fst` 📖	mathematical	—	`HasMFDerivAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.fst` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`Continuous.continuousAt` `continuous_fst` `Filter.mp_mem` `extChartAt_target_mem_nhdsWithin` `Filter.univ_mem'` `PartialEquiv.right_inv` `extChartAt_prod` `HasFDerivWithinAt.congr_of_eventuallyEq` `hasFDerivWithinAt_fst` `PartialEquiv.map_source` `mem_extChartAt_source`
`hasMFDerivAt_id` 📖	mathematical	—	`HasMFDerivAt` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`continuousAt_id` `Filter.mem_of_superset` `extChartAt_target_mem_nhdsWithin` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv` `HasFDerivWithinAt.congr_of_eventuallyEq` `hasFDerivWithinAt_id` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`hasMFDerivAt_inl` 📖	mathematical	—	`HasMFDerivAt` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`hasMFDerivWithinAt_inl`
`hasMFDerivAt_inr` 📖	mathematical	—	`HasMFDerivAt` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`hasMFDerivWithinAt_inr`
`hasMFDerivAt_neg` 📖	mathematical	—	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.neg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `instAddCommGroupTangentSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `neg_neg` `HasMFDerivAt.neg`
`hasMFDerivAt_snd` 📖	mathematical	—	`HasMFDerivAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.snd` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`Continuous.continuousAt` `continuous_snd` `Filter.mp_mem` `extChartAt_target_mem_nhdsWithin` `Filter.univ_mem'` `PartialEquiv.right_inv` `extChartAt_prod` `HasFDerivWithinAt.congr_of_eventuallyEq` `hasFDerivWithinAt_snd` `PartialEquiv.map_source` `mem_extChartAt_source`
`hasMFDerivAt_sumSwap` 📖	mathematical	—	`HasMFDerivAt` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`Continuous.continuousAt` `continuous_sum_swap` `HasFDerivWithinAt.congr_of_eventuallyEq` `hasFDerivWithinAt_id` `writtenInExtChartAt_sumSwap_eventuallyEq_id` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `sum_chartAt_inr_apply` `sum_chartAt_inl_apply`
`hasMFDerivWithinAt_const` 📖	mathematical	—	`HasMFDerivWithinAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	`HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt_const`
`hasMFDerivWithinAt_fst` 📖	mathematical	—	`HasMFDerivWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.fst` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt_fst`
`hasMFDerivWithinAt_id` 📖	mathematical	—	`HasMFDerivWithinAt` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt_id`
`hasMFDerivWithinAt_inl` 📖	mathematical	—	`HasMFDerivWithinAt` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`Continuous.continuousWithinAt` `continuous_inl` `Filter.EventuallyEq.filter_mono` `writtenInExtChartAt_sumInl_eventuallyEq_id` `nhdsWithin_mono` `HasFDerivWithinAt.congr_of_eventuallyEq` `hasFDerivWithinAt_id` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `sum_chartAt_inl_apply`
`hasMFDerivWithinAt_inr` 📖	mathematical	—	`HasMFDerivWithinAt` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`Continuous.continuousWithinAt` `continuous_inr` `Filter.EventuallyEq.filter_mono` `writtenInExtChartAt_sumInr_eventuallyEq_id` `nhdsWithin_mono` `HasFDerivWithinAt.congr_of_eventuallyEq` `hasFDerivWithinAt_id` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `sum_chartAt_inr_apply`
`hasMFDerivWithinAt_snd` 📖	mathematical	—	`HasMFDerivWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.snd` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt_snd`
`mdifferentiableAt_const` 📖	mathematical	—	`MDifferentiableAt`	—	`HasMFDerivAt.mdifferentiableAt` `hasMFDerivAt_const`
`mdifferentiableAt_fst` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`HasMFDerivAt.mdifferentiableAt` `hasMFDerivAt_fst`
`mdifferentiableAt_id` 📖	mathematical	—	`MDifferentiableAt`	—	`HasMFDerivAt.mdifferentiableAt` `hasMFDerivAt_id`
`mdifferentiableAt_neg` 📖	mathematical	—	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`neg_neg` `MDifferentiableAt.neg`
`mdifferentiableAt_prod_iff` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`mdifferentiableWithinAt_prod_iff`
`mdifferentiableAt_prod_module_iff` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `mdifferentiableAt_prod_iff`
`mdifferentiableAt_snd` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`HasMFDerivAt.mdifferentiableAt` `hasMFDerivAt_snd`
`mdifferentiableOn_const` 📖	mathematical	—	`MDifferentiableOn`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable_const`
`mdifferentiableOn_fst` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable_fst`
`mdifferentiableOn_id` 📖	mathematical	—	`MDifferentiableOn`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable_id`
`mdifferentiableOn_prod_iff` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`mdifferentiableWithinAt_prod_iff`
`mdifferentiableOn_prod_module_iff` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `mdifferentiableOn_prod_iff`
`mdifferentiableOn_snd` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable_snd`
`mdifferentiableWithinAt_const` 📖	mathematical	—	`MDifferentiableWithinAt`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_const`
`mdifferentiableWithinAt_fst` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_fst`
`mdifferentiableWithinAt_id` 📖	mathematical	—	`MDifferentiableWithinAt`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_id`
`mdifferentiableWithinAt_prod_iff` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiableWithinAt.fst` `MDifferentiableWithinAt.snd` `MDifferentiableWithinAt.prodMk`
`mdifferentiableWithinAt_prod_module_iff` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `mdifferentiableWithinAt_prod_iff`
`mdifferentiableWithinAt_snd` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_snd`
`mdifferentiable_const` 📖	mathematical	—	`MDifferentiable`	—	`mdifferentiableAt_const`
`mdifferentiable_fst` 📖	mathematical	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`mdifferentiableAt_fst`
`mdifferentiable_id` 📖	mathematical	—	`MDifferentiable`	—	`mdifferentiableAt_id`
`mdifferentiable_prod_iff` 📖	mathematical	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`MDifferentiable.fst` `MDifferentiable.snd` `MDifferentiable.prodMk`
`mdifferentiable_prod_module_iff` 📖	mathematical	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpaceSelf`	—	`modelWithCornersSelf_prod` `chartedSpaceSelf_prod` `mdifferentiable_prod_iff`
`mdifferentiable_snd` 📖	mathematical	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`mdifferentiableAt_snd`
`mfderivWithin_const` 📖	mathematical	—	`mfderivWithin` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	`HasMFDerivWithinAt.mfderivWithin_eq_zero` `hasMFDerivWithinAt_const`
`mfderivWithin_fst` 📖	mathematical	`UniqueMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`mfderivWithin` `ContinuousLinearMap.fst` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`MDifferentiable.mfderivWithin` `mdifferentiableAt_fst` `mfderiv_fst`
`mfderivWithin_id` 📖	mathematical	`UniqueMDiffWithinAt`	`mfderivWithin` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`MDifferentiable.mfderivWithin` `mdifferentiableAt_id` `mfderiv_id`
`mfderivWithin_prodMap` 📖	mathematical	`MDifferentiableWithinAt` `UniqueMDiffWithinAt`	`mfderivWithin` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd` `ContinuousLinearMap.prodMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivWithinAt.mono` `MDifferentiableWithinAt.hasMFDerivWithinAt` `HasMFDerivWithinAt.mfderivWithin` `HasMFDerivWithinAt.prodMap` `UniqueMDiffWithinAt.prod`
`mfderivWithin_prodMk` 📖	mathematical	`MDifferentiableWithinAt` `UniqueMDiffWithinAt`	`mfderivWithin` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivWithinAt.mfderivWithin` `HasMFDerivWithinAt.prodMk` `MDifferentiableWithinAt.hasMFDerivWithinAt`
`mfderivWithin_snd` 📖	mathematical	`UniqueMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`mfderivWithin` `ContinuousLinearMap.snd` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`MDifferentiable.mfderivWithin` `mdifferentiableAt_snd` `mfderiv_snd`
`mfderivWithin_sumInl` 📖	mathematical	`UniqueMDiffWithinAt`	`mfderivWithin` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivWithinAt.mfderivWithin` `hasMFDerivWithinAt_inl`
`mfderivWithin_sumInr` 📖	mathematical	`UniqueMDiffWithinAt`	`mfderivWithin` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivWithinAt.mfderivWithin` `hasMFDerivWithinAt_inr`
`mfderivWithin_sumSwap` 📖	mathematical	`UniqueMDiffWithinAt` `instTopologicalSpaceSum` `ChartedSpace.sum`	`mfderivWithin` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivWithinAt.mfderivWithin` `HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt_sumSwap`
`mfderiv_add` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`mfderiv` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`HasMFDerivAt.mfderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivAt.add` `MDifferentiableAt.hasMFDerivAt`
`mfderiv_const` 📖	mathematical	—	`mfderiv` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	`HasMFDerivAt.mfderiv` `hasMFDerivAt_const`
`mfderiv_fst` 📖	mathematical	—	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.fst` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.mfderiv` `hasMFDerivAt_fst`
`mfderiv_id` 📖	mathematical	—	`mfderiv` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.mfderiv` `hasMFDerivAt_id`
`mfderiv_neg` 📖	mathematical	—	`mfderiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.neg` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace`	—	`HasMFDerivAt.mfderiv` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivAt.neg` `MDifferentiableAt.hasMFDerivAt` `mdifferentiableAt_neg` `neg_zero`
`mfderiv_prodMap` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prodMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`mfderivWithin_prodMap` `MDifferentiableAt.mdifferentiableWithinAt` `uniqueMDiffWithinAt_univ`
`mfderiv_prodMk` 📖	mathematical	`MDifferentiableAt`	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.prod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`mfderivWithin_prodMk` `MDifferentiableAt.mdifferentiableWithinAt` `uniqueMDiffWithinAt_univ`
`mfderiv_prod_eq_add` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`mfderiv` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `RingHomCompTriple.ids` `mfderiv_comp_of_eq` `MDifferentiableAt.prodMk` `mdifferentiableAt_fst` `mdifferentiableAt_const` `mdifferentiableAt_snd` `ContinuousLinearMap.comp_add` `MDifferentiableAt.mfderiv_prod` `mfderiv_fst` `mfderiv_snd` `mfderiv_const` `ContinuousLinearMap.coprod_inl_inr` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.comp_id`
`mfderiv_prod_eq_add_apply` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `RingHomCompTriple.ids` `mfderiv_prod_eq_add_comp`
`mfderiv_prod_eq_add_comp` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	`mfderiv` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearMap.fst` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.toModule` `ContinuousLinearMap.snd`	—	`IsTopologicalAddGroup.toContinuousAdd` `RingHomCompTriple.ids` `mfderiv_prod_eq_add` `mfderiv_comp` `MDifferentiableAt.comp` `MDifferentiableAt.prodMk` `mdifferentiableAt_id` `mdifferentiableAt_const` `mdifferentiableAt_fst` `ContinuousLinearMap.comp.congr_simp` `mfderiv_fst` `mdifferentiableAt_snd` `mfderiv_snd`
`mfderiv_prod_left` 📖	mathematical	—	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.inl` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`MDifferentiableAt.mfderiv_prod` `mdifferentiableAt_id` `mdifferentiableAt_const` `mfderiv_id` `mfderiv_const` `ContinuousLinearMap.inl.eq_1`
`mfderiv_prod_right` 📖	mathematical	—	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.inr` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`MDifferentiableAt.mfderiv_prod` `mdifferentiableAt_const` `mdifferentiableAt_id` `mfderiv_id` `mfderiv_const` `ContinuousLinearMap.inr.eq_1`
`mfderiv_snd` 📖	mathematical	—	`mfderiv` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `ContinuousLinearMap.snd` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.mfderiv` `hasMFDerivAt_snd`
`mfderiv_sub` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf`	`mfderiv` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `NormedSpace.toModule` `ContinuousLinearMap.sub` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `instAddCommGroupTangentSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`HasMFDerivAt.mfderiv` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasMFDerivAt.sub` `MDifferentiableAt.hasMFDerivAt`
`mfderiv_sumInl` 📖	mathematical	—	`mfderiv` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`mfderivWithin_univ` `mfderivWithin_sumInl` `uniqueMDiffWithinAt_univ`
`mfderiv_sumInr` 📖	mathematical	—	`mfderiv` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`mfderivWithin_univ` `mfderivWithin_sumInr` `uniqueMDiffWithinAt_univ`
`mfderiv_sumSwap` 📖	mathematical	—	`mfderiv` `instTopologicalSpaceSum` `ChartedSpace.sum` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`mfderivWithin_univ` `mfderivWithin_sumSwap` `uniqueMDiffWithinAt_univ`
`tangentMapWithin_id` 📖	mathematical	`UniqueMDiffWithinAt` `Bundle.TotalSpace.proj` `TangentSpace`	`tangentMapWithin`	—	`mfderivWithin_id`
`tangentMapWithin_prodFst` 📖	mathematical	`UniqueMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `Bundle.TotalSpace.proj` `TangentSpace`	`tangentMapWithin` `Bundle.TotalSpace.snd`	—	`mfderivWithin_fst`
`tangentMapWithin_prodSnd` 📖	mathematical	`UniqueMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `Bundle.TotalSpace.proj` `TangentSpace`	`tangentMapWithin` `Bundle.TotalSpace.snd`	—	`mfderivWithin_snd`
`tangentMap_id` 📖	mathematical	—	`tangentMap` `TangentBundle`	—	`mfderiv_id`
`tangentMap_prodFst` 📖	mathematical	—	`tangentMap` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `TangentSpace` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd`	—	`mfderiv_fst`
`tangentMap_prodSnd` 📖	mathematical	—	`tangentMap` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `TangentSpace` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd`	—	`mfderiv_snd`
`tangentMap_prod_left` 📖	mathematical	—	`tangentMap` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `TangentSpace` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`mfderiv_prod_left`
`tangentMap_prod_right` 📖	mathematical	—	`tangentMap` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `TangentSpace` `Bundle.TotalSpace.proj` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Bundle.TotalSpace.snd`	—	`mfderiv_prod_right`
`writtenInExtChartAt_sumInl_eventuallyEq_id` 📖	mathematical	—	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.range` `ModelWithCorners.toFun'` `writtenInExtChartAt` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`ModelWithCorners.image_eq` `OpenPartialHomeomorph.extend_image_target_mem_nhds` `mem_chart_source` `Filter.mp_mem` `Filter.univ_mem'` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inl` `ChartedSpace.sum_chartAt_inl` `ModelWithCorners.left_inv` `Function.Injective.extend_apply` `Sum.inl_injective` `OpenPartialHomeomorph.right_inv`
`writtenInExtChartAt_sumInr_eventuallyEq_id` 📖	mathematical	—	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Set.range` `ModelWithCorners.toFun'` `writtenInExtChartAt` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	`ModelWithCorners.image_eq` `OpenPartialHomeomorph.extend_image_target_mem_nhds` `mem_chart_source` `Filter.mp_mem` `Filter.univ_mem'` `nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inr` `ChartedSpace.sum_chartAt_inr` `ModelWithCorners.left_inv` `Function.Injective.extend_apply` `Sum.inr_injective` `OpenPartialHomeomorph.right_inv`
`writtenInExtChartAt_sumSwap_eventuallyEq_id` 📖	mathematical	—	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelWithCorners.toFun'` `OpenPartialHomeomorph.toFun'` `instTopologicalSpaceSum` `chartAt` `ChartedSpace.sum` `Set.range` `writtenInExtChartAt`	—	`nonempty_of_chartedSpace` `Topology.IsOpenEmbedding.inr` `Topology.IsOpenEmbedding.inl` `ChartedSpace.sum_chartAt_inr` `ChartedSpace.sum_chartAt_inl` `Function.Injective.extend_apply` `Sum.inr_injective` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.right_inv` `Filter.eventually_of_mem` `Filter.inter_mem_iff` `ContinuousWithinAt.preimage_mem_nhdsWithin` `ModelWithCorners.continuousWithinAt_symm` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_target` `sum_chartAt_inl_apply` `ModelWithCorners.left_inv` `self_mem_nhdsWithin` `Sum.inl_injective` `sum_chartAt_inr_apply`

---

← Back to Index