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, isExactOn_univ, mono, differentiableOn, with_val_at, isConservativeOn_and_continuousOn_iff_isDifferentiableOn, wedgeIntegral_add_wedgeIntegral_eq, isExactOn_univ, isConservativeOn, isExactOn_ball	12
Total	15

Complex

Definitions

Name	Category	Theorems
IsConservativeOn 📖	MathDef	3 math math: isConservativeOn_and_continuousOn_iff_isDifferentiableOn, IsConservativeOn.mono, DifferentiableOn.isConservativeOn
IsExactOn 📖	MathDef	4 math math: IsConservativeOn.isExactOn_univ, Differentiable.isExactOn_univ, 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 Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring 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 Complex SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Complex.wedgeIntegral nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	Metric.eventually_nhds_iff_ball IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Metric.ball_subset_ball' sub_add_cancel instReflLe Set.mem_of_subset_of_mem ContinuousOn.intervalIntegrable Real.locallyFinite_volume ContinuousOn.comp ContinuousOn.mono ContinuousOn.add_const instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousOn Complex.continuous_ofReal Set.mapsTo_image ContinuousOn.const_add ContinuousOn.mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 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 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 Metric.ball Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	hasDerivAt_wedgeIntegral
isExactOn_univ 📖	mathematical	Continuous Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.IsConservativeOn Set.univ	Complex.IsExactOn Set.univ Complex	—	mono Set.subset_univ hasDerivAt_wedgeIntegral Continuous.continuousOn dist_zero_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
mono 📖	mathematical	Set Complex Set.instHasSubset Complex.IsConservativeOn	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 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	—	DifferentiableAt.differentiableWithinAt HasDerivAt.differentiableAt differentiableOn_congr HasDerivAt.deriv DifferentiableOn.deriv
with_val_at 📖	mathematical	Complex.IsExactOn	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	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul sub_self zero_add

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isExactOn_univ 📖	mathematical	Differentiable 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.IsExactOn Set.univ Complex	—	Complex.IsConservativeOn.isExactOn_univ continuous IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn isOpen_univ differentiableOn

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 Metric.ball Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	Complex.IsConservativeOn.isExactOn_ball continuousOn IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul isConservativeOn

---

← Back to Index