Torsion

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

Statistics

Metric	Count
Definitions torsion, torsion	2
Theorems torsion_antisymm, torsion_apply, torsion_apply_eq_extend, torsion_eq_zero_iff, torsion_self, torsion_antisymm, torsion_apply, torsion_apply_eq_extend, torsion_self	9
Total	11

CovariantDerivative

Definitions

Name	Category	Theorems
torsion 📖	CompOp	5 math math: torsion_apply, torsion_eq_zero_iff, torsion_antisymm, torsion_self, torsion_apply_eq_extend

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
torsion_antisymm 📖	mathematical	—	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsCovariantDerivativeOn.torsion_antisymm isCovariantDerivativeOn
torsion_apply 📖	mathematical	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.mk'	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddCommMonoid toFun instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instContinuousSMulTangentSpace TangentSpace.fiberBundle VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsTopologicalAddGroup.toContinuousAdd smulCommClass_self TensorialAt.mkHom₂_apply
torsion_apply_eq_extend 📖	mathematical	—	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddCommMonoid toFun instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instContinuousSMulTangentSpace TangentSpace.fiberBundle FiberBundle.extend UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsTopologicalAddGroup.toContinuousAdd smulCommClass_self TensorialAt.mkHom₂_apply_eq_extend
torsion_eq_zero_iff 📖	mathematical	—	torsion Pi.instZero 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.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace ContinuousLinearMap.zero MonoidWithZero.toMonoid Semiring.toMonoidWithZero ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid DFunLike.coe AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike toFun instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instContinuousSMulTangentSpace TangentSpace.fiberBundle VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsTopologicalAddGroup.toContinuousAdd smulCommClass_self add_zero torsion_apply ContinuousLinearMap.ext torsion_apply_eq_extend FiberBundle.mdifferentiableAt_extend sub_self
torsion_self 📖	mathematical	—	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsCovariantDerivativeOn.torsion_self isCovariantDerivativeOn

IsCovariantDerivativeOn

Definitions

Name	Category	Theorems
torsion 📖	CompOp	4 math math: torsion_self, torsion_antisymm, torsion_apply_eq_extend, torsion_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
torsion_antisymm 📖	mathematical	IsCovariantDerivativeOn TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instAddCommGroupTangentSpace instModuleTangentSpace instTopologicalSpaceTangentSpace instIsTopologicalAddGroupTangentSpace instContinuousSMulTangentSpace TangentSpace.fiberBundle Set.univ	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsTopologicalAddGroup.toContinuousAdd smulCommClass_self torsion_apply_eq_extend neg_sub VectorField.mlieBracket_swap Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.neg_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval₃ sub_zero Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat
torsion_apply 📖	mathematical	IsCovariantDerivativeOn TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instAddCommGroupTangentSpace instModuleTangentSpace instTopologicalSpaceTangentSpace instIsTopologicalAddGroupTangentSpace instContinuousSMulTangentSpace TangentSpace.fiberBundle Set.univ MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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 TangentSpace instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion SubNegMonoid.toSub AddGroup.toSubNegMonoid VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 TensorialAt.mkHom₂_apply TangentSpace.vectorBundle instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold
torsion_apply_eq_extend 📖	mathematical	IsCovariantDerivativeOn TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instAddCommGroupTangentSpace instModuleTangentSpace instTopologicalSpaceTangentSpace instIsTopologicalAddGroupTangentSpace instContinuousSMulTangentSpace TangentSpace.fiberBundle Set.univ	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion SubNegMonoid.toSub AddGroup.toSubNegMonoid FiberBundle.extend UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 TangentSpace.fiberBundle VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsTopologicalAddGroup.toContinuousAdd smulCommClass_self FiberBundle.extend_apply_self
torsion_self 📖	mathematical	IsCovariantDerivativeOn TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 instAddCommGroupTangentSpace instModuleTangentSpace instTopologicalSpaceTangentSpace instIsTopologicalAddGroupTangentSpace instContinuousSMulTangentSpace TangentSpace.fiberBundle Set.univ	DFunLike.coe 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.funLike ContinuousLinearMap.topologicalSpace instAddCommGroupTangentSpace instIsTopologicalAddGroupTangentSpace 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 instContinuousConstSMulTangentSpace torsion NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 IsTopologicalAddGroup.toContinuousAdd smulCommClass_self torsion_apply_eq_extend sub_self VectorField.mlieBracket_self

---

← Back to Index