SqrtDeriv

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

Statistics

Metric	Count
Definitions	0
Theorems continuousAt_sqrt, continuousOn_sqrt, derivWithin_sqrt, deriv_sqrt, differentiableAt_sqrt, differentiableOn_sqrt, differentiableWithinAt_sqrt, hasDerivAt_sqrt, hasDerivWithinAt_sqrt, hasStrictDerivAt_sqrt	10
Total	10

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_sqrt 📖	mathematical	Real Real.instLE Real.instZero re	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt	—	continuousAt_cpow_const_of_re_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one div_ofNat_re one_div RCLike.charZero_rclike PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing Nat.cast_zero
continuousOn_sqrt 📖	mathematical	—	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt slitPlane	—	ContinuousAt.continuousWithinAt continuousAt_sqrt le_of_lt
derivWithin_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	derivWithin Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt slitPlane DivInvMonoid.toDiv instDivInvMonoid instPow instNeg instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	HasDerivWithinAt.derivWithin Nat.instAtLeastTwoHAddOfNat hasDerivWithinAt_sqrt IsOpen.uniqueDiffWithinAt PerfectSpace.not_isolated instPerfectSpace ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing isOpen_slitPlane
deriv_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	deriv Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt DivInvMonoid.toDiv instDivInvMonoid instPow instNeg instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	HasDerivAt.deriv Nat.instAtLeastTwoHAddOfNat hasDerivAt_sqrt
differentiableAt_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt	—	HasDerivAt.differentiableAt Nat.instAtLeastTwoHAddOfNat hasDerivAt_sqrt
differentiableOn_sqrt 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt slitPlane	—	DifferentiableAt.differentiableWithinAt differentiableAt_sqrt
differentiableWithinAt_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	DifferentiableWithinAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sqrt	—	DifferentiableAt.differentiableWithinAt differentiableAt_sqrt
hasDerivAt_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ContinuousMul.to_continuousSMul NontriviallyNormedField.toNormedField instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing sqrt DivInvMonoid.toDiv instDivInvMonoid instPow instNeg instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	HasStrictDerivAt.hasDerivAt Nat.instAtLeastTwoHAddOfNat hasStrictDerivAt_sqrt
hasDerivWithinAt_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	HasDerivWithinAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ContinuousMul.to_continuousSMul NontriviallyNormedField.toNormedField instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing sqrt DivInvMonoid.toDiv instDivInvMonoid instPow instNeg instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	HasDerivAt.hasDerivWithinAt Nat.instAtLeastTwoHAddOfNat hasDerivAt_sqrt
hasStrictDerivAt_sqrt 📖	mathematical	Complex Set Set.instMembership slitPlane	HasStrictDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ContinuousMul.to_continuousSMul NontriviallyNormedField.toNormedField instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing sqrt DivInvMonoid.toDiv instDivInvMonoid instPow instNeg instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	HasStrictDerivAt.congr_deriv Nat.instAtLeastTwoHAddOfNat hasStrictDerivAt_cpow_const Mathlib.Meta.NormNum.isRat_eq_true Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt mul_comm div_eq_mul_inv

---

← Back to Index