Documentation Verification Report

RealDeriv

📁 Source: Mathlib/Analysis/Complex/RealDeriv.lean

Statistics

Metric	Count
Definitions	0
Theorems `real_of_complex`, `real_of_complex`, `comp_ofReal`, `complexToReal_fderiv`, `complexToReal_fderiv'`, `ofReal_comp`, `real_of_complex`, `complexToReal_fderiv`, `complexToReal_fderiv'`, `complexToReal_fderiv`, `complexToReal_fderiv'`, `real_of_complex`	12
Total	12

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`real_of_complex` 📖	mathematical	`ContDiff` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real` `Real.denselyNormedField` `Real.normedAddCommGroup` `Complex.re` `Complex.ofReal`	—	`contDiff_iff_contDiffAt` `ContDiffAt.real_of_complex` `contDiffAt`

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`real_of_complex` 📖	mathematical	`ContDiffAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `Complex.ofReal`	`Real` `Real.denselyNormedField` `Real.normedAddCommGroup` `Complex.re`	—	`ContDiff.contDiffAt` `ContinuousLinearMap.contDiff` `restrict_scalars` `IsScalarTower.right` `comp`

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_ofReal` 📖	mathematical	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.ofReal`	`Real` `Real.denselyNormedField` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `Complex.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `congr_simp` `mul_one` `comp` `ContinuousLinearMap.hasDerivAt`
`complexToReal_fderiv` 📖	mathematical	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing`	`HasFDerivAt` `Real` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.one`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.restrictScalars_toSpanSingleton` `HasFDerivAt.restrictScalars` `hasFDerivAt`
`complexToReal_fderiv'` 📖	mathematical	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul`	`HasFDerivAt` `Real` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Real.normedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.smulRight` `Real.normedCommRing` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Real.pseudoMetricSpace` `Real.instZero` `Complex.reCLM` `ContinuousLinearMap.instSMul` `Complex.instSemiring` `SMulCommClass.complexToReal` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.I` `Complex.imCLM`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `IsScalarTower.complexToReal` `IsScalarTower.left` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.complexToReal` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.restrictScalars_toSpanSingleton'` `HasFDerivAt.restrictScalars` `hasFDerivAt`
`ofReal_comp` 📖	mathematical	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`Complex` `Complex.addCommGroup` `Complex.instNormedField` `NormedSpace.complexToReal` `IsBoundedSMul.continuousSMul` `Real.instZero` `Complex.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Complex.ofReal`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `congr_simp` `mul_one` `scomp` `IsScalarTower.left` `ContinuousLinearMap.hasDerivAt`
`real_of_complex` 📖	mathematical	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.ofReal`	`Real` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instIsTopologicalRingReal` `Complex.re`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.hasFDerivAt` `LinearMap.IsScalarTower.compatibleSMul'` `IsScalarTower.right` `HasFDerivAt.restrictScalars` `hasFDerivAt` `instIsTopologicalRingReal` `RingHomCompTriple.ids` `congr_simp` `one_mul` `HasFDerivAt.hasDerivAt` `HasFDerivAt.comp`

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complexToReal_fderiv` 📖	mathematical	`HasDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing`	`HasFDerivWithinAt` `Real` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.one`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.restrictScalars_toSpanSingleton` `HasFDerivWithinAt.restrictScalars` `hasFDerivWithinAt`
`complexToReal_fderiv'` 📖	mathematical	`HasDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul`	`HasFDerivWithinAt` `Real` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Real.normedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.smulRight` `Real.normedCommRing` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Real.pseudoMetricSpace` `Real.instZero` `Complex.reCLM` `ContinuousLinearMap.instSMul` `Complex.instSemiring` `SMulCommClass.complexToReal` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.I` `Complex.imCLM`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `IsScalarTower.complexToReal` `IsScalarTower.left` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.complexToReal` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.restrictScalars_toSpanSingleton'` `HasFDerivWithinAt.restrictScalars` `hasFDerivWithinAt`

HasStrictDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complexToReal_fderiv` 📖	mathematical	`HasStrictDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing`	`HasStrictFDerivAt` `Real` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.one`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.restrictScalars_toSpanSingleton` `HasStrictFDerivAt.restrictScalars` `hasStrictFDerivAt`
`complexToReal_fderiv'` 📖	mathematical	`HasStrictDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul`	`HasStrictFDerivAt` `Real` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Real.normedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.smulRight` `Real.normedCommRing` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Real.pseudoMetricSpace` `Real.instZero` `Complex.reCLM` `ContinuousLinearMap.instSMul` `Complex.instSemiring` `SMulCommClass.complexToReal` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.I` `Complex.imCLM`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `IsScalarTower.complexToReal` `IsScalarTower.left` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.complexToReal` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.restrictScalars_toSpanSingleton'` `HasStrictFDerivAt.restrictScalars` `hasStrictFDerivAt`
`real_of_complex` 📖	mathematical	`HasStrictDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMul.to_continuousSMul` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Complex.instSemiring` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.ofReal`	`Real` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Real.pseudoMetricSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instIsTopologicalRingReal` `Complex.re`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.hasStrictFDerivAt` `LinearMap.IsScalarTower.compatibleSMul'` `IsScalarTower.right` `HasStrictFDerivAt.restrictScalars` `hasStrictFDerivAt` `instIsTopologicalRingReal` `RingHomCompTriple.ids` `congr_simp` `one_mul` `HasStrictFDerivAt.hasStrictDerivAt` `HasStrictFDerivAt.comp`

---

← Back to Index