Documentation Verification Report

HasPrimitives

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

Statistics

Metric	Count
Definitions `IsConservativeOn`, `IsExactOn`, `wedgeIntegral`	3
Theorems `eventually_nhds_wedgeIntegral_sub_wedgeIntegral`, `hasDerivAt_wedgeIntegral`, `isExactOn_ball`, `mono`, `differentiableOn`, `isConservativeOn_and_continuousOn_iff_isDifferentiableOn`, `wedgeIntegral_add_wedgeIntegral_eq`, `isConservativeOn`, `isExactOn_ball`	9
Total	12

Complex

Definitions

Name	Category	Theorems
`IsConservativeOn` 📖	MathDef	2 math math: `isConservativeOn_and_continuousOn_iff_isDifferentiableOn`, `DifferentiableOn.isConservativeOn`
`IsExactOn` 📖	MathDef	2 math math: `DifferentiableOn.isExactOn_ball`, `IsConservativeOn.isExactOn_ball`
`wedgeIntegral` 📖	CompOp	3 math math: `wedgeIntegral_add_wedgeIntegral_eq`, `IsConservativeOn.hasDerivAt_wedgeIntegral`, `IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConservativeOn_and_continuousOn_iff_isDifferentiableOn` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	`IsConservativeOn` `ContinuousOn` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`Metric.isOpen_iff` `IsExactOn.differentiableOn` `Metric.isOpen_ball` `IsConservativeOn.isExactOn_ball` `ContinuousOn.mono` `IsConservativeOn.mono` `DifferentiableWithinAt.mono_of_mem_nhdsWithin` `Metric.mem_ball_self` `mem_nhdsWithin` `Set.inter_subset_left` `DifferentiableOn.isConservativeOn` `DifferentiableOn.continuousOn` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`wedgeIntegral_add_wedgeIntegral_eq` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `wedgeIntegral` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `intervalIntegral` `NormedSpace.complexToReal` `Complex` `instAdd` `ofReal` `instMul` `im` `I` `re` `MeasureTheory.MeasureSpace.volume` `Real` `Real.measureSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `instNormedField`	—	`intervalIntegral.integral_symm` `smul_neg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`

Complex.IsConservativeOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_nhds_wedgeIntegral_sub_wedgeIntegral` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.ball` `Set` `Set.instMembership` `Complex.IsConservativeOn`	`Filter.Eventually` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Complex.wedgeIntegral` `nhds`	—	`Metric.eventually_nhds_iff_ball` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Metric.ball_subset_ball'` `sub_add_cancel` `Set.mem_of_subset_of_mem` `ContinuousOn.intervalIntegrable` `Real.locallyFinite_volume` `ContinuousOn.comp` `ContinuousOn.mono` `ContinuousOn.fun_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.continuousOn` `Complex.continuous_ofReal` `continuousOn_const` `Set.mapsTo_image` `ContinuousOn.fun_mul` `IsTopologicalSemiring.toContinuousMul` `intervalIntegral.integral_add_adjacent_intervals` `Metric.mem_ball_self` `Metric.pos_of_mem_ball` `smul_add` `Complex.re_add_im` `Complex.Convex.rectangle_subset` `convex_ball` `MulZeroClass.mul_zero` `mul_one` `sub_self` `add_zero` `zero_add` `Complex.wedgeIntegral_add_wedgeIntegral_eq`
`hasDerivAt_wedgeIntegral` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.ball` `Set` `Set.instMembership` `Complex.IsConservativeOn`	`HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `IsBoundedSMul.continuousSMul` `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` `Complex.wedgeIntegral`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_iff_isLittleO` `Filter.Eventually.mono` `eventually_nhds_wedgeIntegral_sub_wedgeIntegral` `Complex.re_add_im` `Complex.ofReal_sub` `add_smul` `smul_sub` `smul_smul` `mul_comm` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `Asymptotics.IsLittleO.add` `Asymptotics.IsLittleO.const_smul_left`
`isExactOn_ball` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.ball` `Complex.IsConservativeOn`	`Complex.IsExactOn`	—	`hasDerivAt_wedgeIntegral`
`mono` 📖	—	`Set` `Complex` `Set.instHasSubset` `Complex.IsConservativeOn`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`

Complex.IsExactOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableOn` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.IsExactOn`	`DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`DifferentiableAt.differentiableWithinAt` `HasDerivAt.differentiableAt` `differentiableOn_congr` `HasDerivAt.deriv` `DifferentiableOn.deriv`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConservativeOn` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Complex.IsConservativeOn`	—	`add_eq_zero_iff_eq_neg` `Complex.wedgeIntegral_add_wedgeIntegral_eq` `Complex.integral_boundary_rect_eq_zero_of_differentiableOn` `mono`
`isExactOn_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball`	`Complex.IsExactOn`	—	`Complex.IsConservativeOn.isExactOn_ball` `continuousOn` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `isConservativeOn`

---

← Back to Index