Basic

📁 Source: Mathlib/Analysis/Calculus/Gradient/Basic.lean

Statistics

Metric	Count
Definitions `«term∇»`, `HasGradientAt`, `HasGradientAtFilter`, `HasGradientWithinAt`, `gradient`, `gradientWithin`	6
Theorems `hasGradientAt`, `hasGradientAt`, `hasGradientWithinAt`, `gradient`, `gradient_eq`, `hasGradientAtFilter_iff`, `hasGradientAt`, `hasGradientAt'`, `hasGradientAtFilter`, `hasGradientAtFilter'`, `hasGradientAt`, `hasGradientWithinAt`, `congr_of_eventuallyEq`, `continuousAt`, `continuousOn`, `differentiableAt`, `fderiv_apply`, `gradient`, `hasDerivAt`, `hasDerivAt'`, `hasFDerivAt`, `unique`, `congr_of_eventuallyEq`, `hasDerivAtFilter`, `hasDerivAtFilter'`, `isBigO_sub`, `tendsto_nhds`, `congr_mono`, `congr_of_eventuallyEq`, `congr_of_eventuallyEq_of_mem`, `congr_of_mem`, `continuousWithinAt`, `differentiableWithinAt`, `fderivWithin_apply`, `hasFDerivWithinAt`, `gradient_const`, `gradient_const'`, `gradient_eq`, `gradient_eq_deriv`, `gradient_eq_deriv'`, `gradient_eq_zero_of_not_differentiableAt`, `gradient_fun_const`, `gradient_fun_const'`, `hasFDerivAt_iff_hasGradientAt`, `hasFDerivWithinAt_iff_hasGradientWithinAt`, `hasGradientAtFilter_const`, `hasGradientAtFilter_iff_isLittleO`, `hasGradientAt_const`, `hasGradientAt_iff_hasFDerivAt`, `hasGradientAt_iff_isLittleO`, `hasGradientAt_iff_isLittleO_nhds_zero`, `hasGradientAt_iff_tendsto`, `hasGradientWithinAt_congr_set`, `hasGradientWithinAt_congr_set'`, `hasGradientWithinAt_const`, `hasGradientWithinAt_iff_hasFDerivWithinAt`, `hasGradientWithinAt_iff_isLittleO`, `hasGradientWithinAt_iff_tendsto`, `hasGradientWithinAt_univ`, `inner_gradientWithin_left`, `inner_gradientWithin_right`, `inner_gradient_left`, `inner_gradient_right`	63
Total	69

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientAt` 📖	mathematical	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	`HasGradientAt` `gradient`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientAt_iff_hasFDerivAt` `gradient.eq_1` `LinearIsometryEquiv.apply_symm_apply` `hasFDerivAt`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientAt` 📖	mathematical	`DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Set` `Filter` `Filter.instMembership` `nhds`	`HasGradientAt` `gradient`	—	`HasFDerivAt.hasGradientAt` `hasFDerivAt`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientWithinAt` 📖	mathematical	`DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	`HasGradientWithinAt` `gradientWithin`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientWithinAt_iff_hasFDerivWithinAt` `gradientWithin.eq_1` `LinearIsometryEquiv.apply_symm_apply` `hasFDerivWithinAt`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gradient` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`gradient`	—	`Filter.Eventually.mono` `eventuallyEq_nhds` `gradient_eq`
`gradient_eq` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`gradient`	—	`fderiv_eq`
`hasGradientAtFilter_iff` 📖	mathematical	`Filter.EventuallyEq`	`HasGradientAtFilter`	—	`hasFDerivAtFilter_iff`

Gradient

Definitions

Name	Category	Theorems
`«term∇»` 📖	CompOp	—

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientAt` 📖	mathematical	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsModuleTopology.toContinuousSMul` `NontriviallyNormedField.toNormedField` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing`	`HasGradientAt` `RCLike.toCompleteSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.toCompleteSpace` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientAt_iff_hasFDerivAt` `hasFDerivAt_iff_hasDerivAt` `congr_simp` `RingHomCompTriple.comp_apply` `RingHomInvPair.triples₂` `one_mul`
`hasGradientAt'` 📖	mathematical	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`HasGradientAt` `Real.normedAddCommGroup` `Real.instCompleteSpace`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasGradientAt`

HasDerivAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientAtFilter` 📖	mathematical	`HasDerivAtFilter` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsModuleTopology.toContinuousSMul` `NontriviallyNormedField.toNormedField` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing`	`HasGradientAtFilter` `RCLike.toCompleteSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsScalarTower.right` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RCLike.toCompleteSpace` `ContinuousLinearMap.ext_ring` `one_mul` `RingHomCompTriple.comp_apply` `RingHomInvPair.triples₂` `HasGradientAtFilter.eq_1`
`hasGradientAtFilter'` 📖	mathematical	`HasDerivAtFilter` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`HasGradientAtFilter` `Real.normedAddCommGroup` `Real.instCompleteSpace`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasGradientAtFilter`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientAt` 📖	mathematical	`HasFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`HasGradientAt` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `InnerProductSpace.toDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasFDerivAt_iff_hasGradientAt`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGradientWithinAt` 📖	mathematical	`HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`HasGradientWithinAt` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `InnerProductSpace.toDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasFDerivWithinAt_iff_hasGradientWithinAt`

HasGradientAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_of_eventuallyEq` 📖	—	`HasGradientAt` `Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`HasGradientAtFilter.congr_of_eventuallyEq` `mem_of_mem_nhds`
`continuousAt` 📖	mathematical	`HasGradientAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`HasGradientAtFilter.tendsto_nhds` `le_rfl`
`continuousOn` 📖	mathematical	`HasGradientAt`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`ContinuousAt.continuousWithinAt` `continuousAt`
`differentiableAt` 📖	mathematical	`HasGradientAt`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	—	`HasFDerivAt.differentiableAt` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasFDerivAt`
`fderiv_apply` 📖	mathematical	`HasGradientAt`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.funLike` `fderiv` `Inner.inner` `InnerProductSpace.toInner`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasFDerivAt.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt` `InnerProductSpace.toDual_apply_apply`
`gradient` 📖	mathematical	`HasGradientAt`	`gradient`	—	`unique` `DifferentiableAt.hasGradientAt` `differentiableAt`
`hasDerivAt` 📖	mathematical	`HasGradientAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.toCompleteSpace`	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsModuleTopology.toContinuousSMul` `NontriviallyNormedField.toNormedField` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`RCLike.toCompleteSpace` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasDerivAt.congr_simp` `one_mul` `hasFDerivAt_iff_hasDerivAt` `hasGradientAt_iff_hasFDerivAt`
`hasDerivAt'` 📖	mathematical	`HasGradientAt` `Real` `Real.instRCLike` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace`	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	—	`Real.instCompleteSpace` `hasDerivAt`
`hasFDerivAt` 📖	mathematical	`HasGradientAt`	`HasFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `InnerProductSpace.toDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientAt_iff_hasFDerivAt`
`unique` 📖	—	`HasGradientAt`	—	—	`LinearIsometryEquiv.injective` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasFDerivAt.unique` `IsTopologicalAddGroup.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt`

HasGradientAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_of_eventuallyEq` 📖	—	`HasGradientAtFilter` `Filter.EventuallyEq`	—	—	`Filter.EventuallyEq.hasGradientAtFilter_iff`
`hasDerivAtFilter` 📖	mathematical	`HasGradientAtFilter` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.toCompleteSpace`	`HasDerivAtFilter` `DenselyNormedField.toNontriviallyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsModuleTopology.toContinuousSMul` `NontriviallyNormedField.toNormedField` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`RCLike.toCompleteSpace`
`hasDerivAtFilter'` 📖	mathematical	`HasGradientAtFilter` `Real` `Real.instRCLike` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace`	`HasDerivAtFilter` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	—	`Real.instCompleteSpace` `hasDerivAtFilter`
`isBigO_sub` 📖	mathematical	`HasGradientAtFilter`	`Asymptotics.IsBigO` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`HasFDerivAtFilter.isBigO_sub`
`tendsto_nhds` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasGradientAtFilter`	`Filter.Tendsto` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`HasFDerivAtFilter.tendsto_nhds` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology`

HasGradientWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_mono` 📖	—	`HasGradientWithinAt` `Set` `Set.instHasSubset`	—	—	`HasFDerivWithinAt.congr_mono`
`congr_of_eventuallyEq` 📖	—	`HasGradientWithinAt` `Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`HasGradientAtFilter.congr_of_eventuallyEq`
`congr_of_eventuallyEq_of_mem` 📖	—	`HasGradientWithinAt` `Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	—	—	`congr_of_eventuallyEq` `Filter.EventuallyEq.eq_of_nhdsWithin`
`congr_of_mem` 📖	—	`HasGradientWithinAt` `Set` `Set.instMembership`	—	—	`congr`
`continuousWithinAt` 📖	mathematical	`HasGradientWithinAt`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`HasGradientAtFilter.tendsto_nhds` `inf_le_left`
`differentiableWithinAt` 📖	mathematical	`HasGradientWithinAt`	`DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	—	`HasFDerivWithinAt.differentiableWithinAt` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasFDerivWithinAt`
`fderivWithin_apply` 📖	mathematical	`HasGradientWithinAt` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DFunLike.coe` `ContinuousLinearMap` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.funLike` `fderivWithin` `Inner.inner` `InnerProductSpace.toInner`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasFDerivWithinAt.fderivWithin` `IsTopologicalAddGroup.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalSemiring.toContinuousAdd` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivWithinAt` `InnerProductSpace.toDual_apply_apply`
`hasFDerivWithinAt` 📖	mathematical	`HasGradientWithinAt`	`HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `InnerProductSpace.toDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientWithinAt_iff_hasFDerivWithinAt`

(root)

Definitions

Name	Category	Theorems
`HasGradientAt` 📖	MathDef	12 math math: `hasFDerivAt_iff_hasGradientAt`, `HasDerivAt.hasGradientAt`, `hasGradientAt_iff_isLittleO`, `hasGradientAt_iff_isLittleO_nhds_zero`, `hasGradientAt_const`, `DifferentiableAt.hasGradientAt`, `hasGradientAt_iff_tendsto`, `hasGradientWithinAt_univ`, `hasGradientAt_iff_hasFDerivAt`, `HasDerivAt.hasGradientAt'`, `DifferentiableOn.hasGradientAt`, `HasFDerivAt.hasGradientAt`
`HasGradientAtFilter` 📖	MathDef	5 math math: `hasGradientAtFilter_const`, `hasGradientAtFilter_iff_isLittleO`, `HasDerivAtFilter.hasGradientAtFilter`, `Filter.EventuallyEq.hasGradientAtFilter_iff`, `HasDerivAtFilter.hasGradientAtFilter'`
`HasGradientWithinAt` 📖	MathDef	10 math math: `hasGradientWithinAt_iff_hasFDerivWithinAt`, `HasFDerivWithinAt.hasGradientWithinAt`, `hasGradientWithinAt_univ`, `hasFDerivWithinAt_iff_hasGradientWithinAt`, `hasGradientWithinAt_congr_set`, `hasGradientWithinAt_congr_set'`, `hasGradientWithinAt_iff_tendsto`, `hasGradientWithinAt_iff_isLittleO`, `DifferentiableWithinAt.hasGradientWithinAt`, `hasGradientWithinAt_const`
`gradient` 📖	CompOp	15 math math: `gradient_fun_const`, `Filter.EventuallyEq.gradient`, `gradient_eq_deriv'`, `DifferentiableAt.hasGradientAt`, `Filter.EventuallyEq.gradient_eq`, `gradient_const`, `gradient_const'`, `gradient_fun_const'`, `HasGradientAt.gradient`, `DifferentiableOn.hasGradientAt`, `gradient_eq`, `inner_gradient_left`, `gradient_eq_deriv`, `inner_gradient_right`, `gradient_eq_zero_of_not_differentiableAt`
`gradientWithin` 📖	CompOp	3 math math: `inner_gradientWithin_right`, `inner_gradientWithin_left`, `DifferentiableWithinAt.hasGradientWithinAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gradient_const` 📖	mathematical	—	`gradient` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`gradient_fun_const`
`gradient_const'` 📖	mathematical	—	`gradient` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`gradient_fun_const'`
`gradient_eq` 📖	mathematical	`HasGradientAt`	`gradient`	—	`HasGradientAt.gradient`
`gradient_eq_deriv` 📖	mathematical	—	`gradient` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.toCompleteSpace` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `deriv` `DenselyNormedField.toNontriviallyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	—	`RCLike.toCompleteSpace` `HasDerivAt.deriv` `HasGradientAt.hasDerivAt` `DifferentiableAt.hasGradientAt` `RCLike.conj_conj` `gradient_eq_zero_of_not_differentiableAt` `deriv_zero_of_not_differentiableAt` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`gradient_eq_deriv'` 📖	mathematical	—	`gradient` `Real` `Real.instRCLike` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`gradient_eq_deriv`
`gradient_eq_zero_of_not_differentiableAt` 📖	mathematical	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	`gradient` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`gradient.eq_1` `fderiv_zero_of_not_differentiableAt` `map_zero` `AddMonoidHomClass.toZeroHomClass` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `RingHomIsometric.ids` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass`
`gradient_fun_const` 📖	mathematical	—	`gradient` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`fderiv_fun_const` `map_zero` `AddMonoidHomClass.toZeroHomClass` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `RingHomIsometric.ids` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass`
`gradient_fun_const'` 📖	mathematical	—	`gradient` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`gradient_const`
`hasFDerivAt_iff_hasGradientAt` 📖	mathematical	—	`HasFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `HasGradientAt` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `InnerProductSpace.toDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientAt_iff_hasFDerivAt` `LinearIsometryEquiv.apply_symm_apply`
`hasFDerivWithinAt_iff_hasGradientWithinAt` 📖	mathematical	—	`HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `HasGradientWithinAt` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `InnerProductSpace.toDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientWithinAt_iff_hasFDerivWithinAt` `LinearIsometryEquiv.apply_symm_apply`
`hasGradientAtFilter_const` 📖	mathematical	—	`HasGradientAtFilter` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`HasGradientAtFilter.eq_1` `map_zero` `AddMonoidHomClass.toZeroHomClass` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `RingHomIsometric.ids` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `hasFDerivAtFilter_const`
`hasGradientAtFilter_iff_isLittleO` 📖	mathematical	—	`HasGradientAtFilter` `Asymptotics.IsLittleO` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`hasFDerivAtFilter_iff_isLittleO`
`hasGradientAt_const` 📖	mathematical	—	`HasGradientAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`hasGradientAtFilter_const`
`hasGradientAt_iff_hasFDerivAt` 📖	mathematical	—	`HasGradientAt` `HasFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `InnerProductSpace.toDual`	—	—
`hasGradientAt_iff_isLittleO` 📖	mathematical	—	`HasGradientAt` `Asymptotics.IsLittleO` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner`	—	`hasGradientAtFilter_iff_isLittleO`
`hasGradientAt_iff_isLittleO_nhds_zero` 📖	mathematical	—	`HasGradientAt` `Asymptotics.IsLittleO` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Inner.inner` `InnerProductSpace.toInner`	—	`hasFDerivAt_iff_isLittleO_nhds_zero`
`hasGradientAt_iff_tendsto` 📖	mathematical	—	`HasGradientAt` `Filter.Tendsto` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`hasFDerivAtFilter_iff_tendsto`
`hasGradientWithinAt_congr_set` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasGradientWithinAt`	—	`hasFDerivWithinAt_congr_set`
`hasGradientWithinAt_congr_set'` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`HasGradientWithinAt`	—	`hasFDerivWithinAt_congr_set'` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`hasGradientWithinAt_const` 📖	mathematical	—	`HasGradientWithinAt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`hasGradientAtFilter_const`
`hasGradientWithinAt_iff_hasFDerivWithinAt` 📖	mathematical	—	`HasGradientWithinAt` `HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Semiring.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `InnerProductSpace.toDual`	—	—
`hasGradientWithinAt_iff_isLittleO` 📖	mathematical	—	`HasGradientWithinAt` `Asymptotics.IsLittleO` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toNorm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner`	—	`hasGradientAtFilter_iff_isLittleO`
`hasGradientWithinAt_iff_tendsto` 📖	mathematical	—	`HasGradientWithinAt` `Filter.Tendsto` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `nhds` `Real.pseudoMetricSpace` `Real.instZero`	—	`hasFDerivAtFilter_iff_tendsto`
`hasGradientWithinAt_univ` 📖	mathematical	—	`HasGradientWithinAt` `Set.univ` `HasGradientAt`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasGradientWithinAt_iff_hasFDerivWithinAt` `hasGradientAt_iff_hasFDerivAt` `hasFDerivWithinAt_univ`
`inner_gradientWithin_left` 📖	mathematical	`DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	`Inner.inner` `InnerProductSpace.toInner` `gradientWithin` `DFunLike.coe` `ContinuousLinearMap` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderivWithin`	—	`HasGradientWithinAt.fderivWithin_apply` `DifferentiableWithinAt.hasGradientWithinAt`
`inner_gradientWithin_right` 📖	mathematical	`DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	`Inner.inner` `InnerProductSpace.toInner` `gradientWithin` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderivWithin`	—	`inner_conj_symm` `inner_gradientWithin_left`
`inner_gradient_left` 📖	mathematical	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	`Inner.inner` `InnerProductSpace.toInner` `gradient` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderiv`	—	`HasGradientAt.fderiv_apply` `DifferentiableAt.hasGradientAt`
`inner_gradient_right` 📖	mathematical	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing`	`Inner.inner` `InnerProductSpace.toInner` `gradient` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `fderiv`	—	`inner_conj_symm` `HasGradientAt.fderiv_apply` `DifferentiableAt.hasGradientAt`

---

← Back to Index