Documentation Verification Report

Basic

📁 Source: Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

Statistics

Metric	Count
Definitions `ContMDiffCovariantDerivativeOn`, `CovariantDerivative`, `ContMDiffCovariantDerivative`, `addOneForm`, `affine_combination`, `difference`, `finite_affine_combination`, `instCoeFunForallForallForallContinuousLinearMapIdTangentSpace`, `of_isCovariantDerivativeOn_of_open_cover`, `toFun`, `IsCovariantDerivativeOn`, `difference`	12
Theorems `affine_combination`, `contMDiff`, `finite_affine_combination`, `affine_combination`, `contMDiff`, `finite_affine_combination`, `affine_combination_toFun`, `contMDiffCovariantDerivativeOn_univ_iff`, `ext`, `ext_iff`, `isCovariantDerivativeOn`, `isCovariantDerivativeOnUniv`, `of_isCovariantDerivativeOn_of_open_cover_coe`, `zero`, `add`, `add_one_form`, `affine_combination`, `congr_of_eqOn`, `congr_of_eventuallyEq`, `difference_apply`, `finite_affine_combination`, `iUnion`, `leibniz`, `mono`, `smul_const`, `zero`	26
Total	38

ContMDiffCovariantDerivativeOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affine_combination` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `modelWithCornersSelf` `chartedSpaceSelf`	`ContMDiffCovariantDerivativeOn` `Pi.instAdd` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `Pi.smul'` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `Pi.instSub` `SubNegMonoid.toSub` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `ContMDiffOn.add_section` `RingHomIsometric.ids` `TangentSpace.vectorBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContMDiffOn.smul_section` `contMDiff` `ContMDiffOn.sub` `instNormedSpaceLieAddGroup` `contMDiffOn_const`
`contMDiff` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `WithTop` `ENat` `WithTop.add` `instAddENat` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `Bundle.TotalSpace.mk'`	`ContMDiffOn` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentSpace` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `instAddCommGroupTangentSpace` `instTopologicalSpaceTangentBundle` `TangentSpace.fiberBundle` `TangentSpace.vectorBundle` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle`	—	—
`finite_affine_combination` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffCovariantDerivativeOn` `ContMDiffOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `modelWithCornersSelf` `chartedSpaceSelf`	`ContMDiffCovariantDerivativeOn` `Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `RingHomIsometric.ids` `TangentSpace.vectorBundle` `Finset.sum_congr` `ContMDiffOn.sum_section` `Bundle.ContinuousLinearMap.vectorBundle` `ContMDiffOn.smul_section` `contMDiff`

CovariantDerivative

Definitions

Name	Category	Theorems
`ContMDiffCovariantDerivative` 📖	CompData	3 math math: `ContMDiffCovariantDerivative.finite_affine_combination`, `ContMDiffCovariantDerivative.affine_combination`, `contMDiffCovariantDerivativeOn_univ_iff`
`addOneForm` 📖	CompOp	—
`affine_combination` 📖	CompOp	2 math math: `affine_combination_toFun`, `ContMDiffCovariantDerivative.affine_combination`
`difference` 📖	CompOp	—
`finite_affine_combination` 📖	CompOp	1 math math: `ContMDiffCovariantDerivative.finite_affine_combination`
`instCoeFunForallForallForallContinuousLinearMapIdTangentSpace` 📖	CompOp	—
`of_isCovariantDerivativeOn_of_open_cover` 📖	CompOp	1 math math: `of_isCovariantDerivativeOn_of_open_cover_coe`
`toFun` 📖	CompOp	11 math math: `isCovariantDerivativeOn`, `of_isCovariantDerivativeOn_of_open_cover_coe`, `torsion_apply`, `affine_combination_toFun`, `zero`, `isCovariantDerivativeOnUniv`, `torsion_eq_zero_iff`, `ContMDiffCovariantDerivative.contMDiff`, `contMDiffCovariantDerivativeOn_univ_iff`, `torsion_apply_eq_extend`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affine_combination_toFun` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`toFun` `affine_combination` `Pi.instAdd` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `Pi.smul'` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Pi.instSub` `SubNegMonoid.toSub` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	—
`contMDiffCovariantDerivativeOn_univ_iff` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`ContMDiffCovariantDerivativeOn` `toFun` `Set.univ` `ContMDiffCovariantDerivative`	—	`ContMDiffCovariantDerivative.contMDiff`
`ext` 📖	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toFun`	—	—	—
`ext_iff` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`toFun`	—	`ext`
`isCovariantDerivativeOn` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`IsCovariantDerivativeOn` `toFun`	—	`IsCovariantDerivativeOn.mono` `isCovariantDerivativeOnUniv`
`isCovariantDerivativeOnUniv` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`IsCovariantDerivativeOn` `toFun` `Set.univ`	—	—
`of_isCovariantDerivativeOn_of_open_cover_coe` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `Set.iUnion` `Set.univ`	`toFun` `of_isCovariantDerivativeOn_of_open_cover`	—	—
`zero` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`toFun` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	`IsCovariantDerivativeOn.zero` `isCovariantDerivativeOnUniv`

CovariantDerivative.ContMDiffCovariantDerivative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affine_combination` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiff` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `modelWithCornersSelf` `chartedSpaceSelf`	`CovariantDerivative.ContMDiffCovariantDerivative` `CovariantDerivative.affine_combination`	—	`ContMDiffCovariantDerivativeOn.affine_combination` `ContMDiff.contMDiffOn` `contMDiff`
`contMDiff` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`ContMDiffCovariantDerivativeOn` `CovariantDerivative.toFun` `Set.univ`	—	—
`finite_affine_combination` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContMDiff` `NormedField.toNormedSpace` `modelWithCornersSelf` `chartedSpaceSelf` `CovariantDerivative.ContMDiffCovariantDerivative`	`CovariantDerivative.ContMDiffCovariantDerivative` `CovariantDerivative.finite_affine_combination`	—	`ContMDiffCovariantDerivativeOn.finite_affine_combination` `contMDiff` `ContMDiff.contMDiffOn`

IsCovariantDerivativeOn

Definitions

Name	Category	Theorems
`difference` 📖	CompOp	1 math math: `difference_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `Set` `Set.univ` `Set.instMembership`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup`	—	—
`add_one_form` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn`	`IsCovariantDerivativeOn` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `DFunLike.coe` `ContinuousLinearMap.topologicalSpace` `instAddCommGroupTangentSpace` `ContinuousLinearMap.addCommMonoid` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `add` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `IsScalarTower.left` `leibniz` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `smul_add` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `add_zero` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`affine_combination` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn`	`IsCovariantDerivativeOn` `Pi.instAdd` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `Pi.smul'` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `Pi.instSub` `SubNegMonoid.toSub` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `add` `smul_add` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_one` `IsScalarTower.left` `leibniz` `add_zero` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`congr_of_eqOn` 📖	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `Set` `Filter` `Filter.instMembership` `nhds`	—	—	`mem_of_mem_nhds` `one_smul` `zero_smul` `hasMFDerivAt_const` `HasMFDerivAt.congr_of_eventuallyEq` `Filter.eventuallyEq_of_mem` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsScalarTower.left` `leibniz` `HasMFDerivAt.mdifferentiableAt` `ContinuousLinearMap.smulRight.congr_simp` `ContinuousLinearMap.comp.congr_simp` `HasMFDerivAt.mfderiv` `ContinuousLinearMap.comp_zero` `ContinuousLinearMap.zero_smulRight` `add_zero`
`congr_of_eventuallyEq` 📖	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `Set` `Filter` `Filter.instMembership` `nhds` `Filter.Eventually`	—	—	`congr_of_eqOn` `mono` `Set.inter_subset_left` `Filter.inter_mem` `Filter.eventually_iff_exists_mem`
`difference_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `Set` `Set.instMembership` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.topologicalSpace` `instAddCommGroupTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ContinuousLinearMap.funLike` `difference` `ContinuousLinearMap.sub` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `TensorialAt.mkHom_apply`
`finite_affine_combination` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	`IsCovariantDerivativeOn` `Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `Finset.sum_add_distrib` `ContinuousLinearMap.ext` `smul_add` `add` `IsScalarTower.left` `Finset.sum_congr` `leibniz` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Finset.smul_sum` `Finset.sum_apply` `Finset.sum_smul` `one_smul`
`iUnion` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn`	`IsCovariantDerivativeOn` `Set.iUnion`	—	`IsTopologicalAddGroup.toContinuousAdd` `add` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsScalarTower.left` `leibniz`
`leibniz` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedSpace` `chartedSpaceSelf` `Set` `Set.univ` `Set.instMembership`	`Pi.smul'` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.instSMul` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `AddZero.toZero` `AddZeroClass.toAddZero` `ContinuousLinearMap.smulRight` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `IsScalarTower.left` `extDerivFun`	—	—
`mono` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `Set` `Set.instHasSubset`	`IsCovariantDerivativeOn`	—	`add` `leibniz`
`smul_const` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `Set` `Set.instMembership`	`Pi.instSMul` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.instSMul` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsScalarTower.left` `ContinuousLinearMap.smulRight.congr_simp` `ContinuousLinearMap.comp.congr_simp` `mfderiv_const` `ContinuousLinearMap.comp_zero` `ContinuousLinearMap.zero_smulRight` `add_zero` `leibniz` `mdifferentiableAt_const`
`zero` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsCovariantDerivativeOn` `Set` `Set.instMembership`	`Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.zero`	—	`IsTopologicalAddGroup.toContinuousAdd` `add_zero` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add` `Bundle.mdifferentiableAt_zeroSection`

(root)

Definitions

Name	Category	Theorems
`ContMDiffCovariantDerivativeOn` 📖	CompData	4 math math: `ContMDiffCovariantDerivativeOn.affine_combination`, `ContMDiffCovariantDerivativeOn.finite_affine_combination`, `CovariantDerivative.ContMDiffCovariantDerivative.contMDiff`, `CovariantDerivative.contMDiffCovariantDerivativeOn_univ_iff`
`CovariantDerivative` 📖	CompData	—
`IsCovariantDerivativeOn` 📖	CompData	7 math math: `CovariantDerivative.isCovariantDerivativeOn`, `CovariantDerivative.isCovariantDerivativeOnUniv`, `IsCovariantDerivativeOn.add_one_form`, `IsCovariantDerivativeOn.mono`, `IsCovariantDerivativeOn.affine_combination`, `IsCovariantDerivativeOn.finite_affine_combination`, `IsCovariantDerivativeOn.iUnion`

---

← Back to Index