VectorField

📁 Source: Mathlib/Analysis/Calculus/DifferentialForm/VectorField.lean

Statistics

Metric	Count
Definitions	0
Theorems extDerivWithin_apply_vectorField, extDerivWithin_apply_vectorField_of_pairwise_commute, extDeriv_apply_vectorField, extDeriv_apply_vectorField_of_pairwise_commute	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extDerivWithin_apply_vectorField 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousAlternatingMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousAlternatingMap.instTopologicalSpace UniqueDiffWithinAt	DFunLike.coe ContinuousAlternatingMap.funLike extDerivWithin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Finset.sum Finset.univ Fin.fintype SubNegMonoid.toZSMul Monoid.toNatPow Int.instMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin Fin.removeNth Finset.Ici PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop Matrix.vecCons VectorField.lieBracketWithin	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Finset.sum_congr fderivWithin_continuousAlternatingMap_apply_apply smul_add Finset.smul_sum Finset.sum_add_distrib add_sub_assoc extDerivWithin_apply fderivWithin_continuousAlternatingMap_apply_const_apply Finite.of_fintype AddLeftCancelSemigroup.toIsLeftCancelAdd Fin.sum_sum_eq_sum_triangle_add Fintype.sum_congr ContinuousAlternatingMap.map_insertNth Fin.removeNth_removeNth_eq_swap Fin.succAbove_of_le_castSucc Finset.mem_Ici Fin.predAbove_of_le_castSucc Fin.succAbove_of_castSucc_lt pow_add pow_one mul_neg mul_one neg_smul SMulCommClass.smul_comm AddGroup.int_smulCommClass ContinuousAlternatingMap.map_vecCons_sub smul_sub SemigroupAction.mul_smul
extDerivWithin_apply_vectorField_of_pairwise_commute 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousAlternatingMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousAlternatingMap.instTopologicalSpace UniqueDiffWithinAt Pairwise VectorField.lieBracketWithin	DFunLike.coe ContinuousAlternatingMap.funLike extDerivWithin Finset.sum Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Monoid.toNatPow Int.instMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin Fin.removeNth	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self extDerivWithin_apply Finset.sum_congr Finset.univ_unique pow_zero fderivWithin_continuousAlternatingMap_apply_const_apply Finite.of_fintype one_smul Finset.sum_singleton Fin.removeNth_zero fderivWithin_continuousAlternatingMap_apply_apply Fin.isEmpty' Finset.univ_eq_empty add_zero extDerivWithin_apply_vectorField sub_eq_self Fintype.sum_eq_zero Finset.sum_eq_zero ne_of_lt ContinuousAlternatingMap.map_coord_zero smul_zero
extDeriv_apply_vectorField 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousAlternatingMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousAlternatingMap.instTopologicalSpace	DFunLike.coe ContinuousAlternatingMap.funLike extDeriv SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Finset.sum Finset.univ Fin.fintype SubNegMonoid.toZSMul Monoid.toNatPow Int.instMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv Fin.removeNth Finset.Ici PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop Matrix.vecCons VectorField.lieBracket	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Finset.sum_congr extDerivWithin_apply_vectorField PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul
extDeriv_apply_vectorField_of_pairwise_commute 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousAlternatingMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousAlternatingMap.instTopologicalSpace Pairwise VectorField.lieBracket	DFunLike.coe ContinuousAlternatingMap.funLike extDeriv Finset.sum Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Monoid.toNatPow Int.instMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv Fin.removeNth	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Finset.sum_congr extDerivWithin_apply_vectorField_of_pairwise_commute PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul

---

← Back to Index