Documentation Verification Report

AffineSpace

📁 Source: Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean

Statistics

Metric	Count
Definitions `convexCombination`, `instConvexSpace`	2
Theorems `convexCombination_assoc`, `convexCombination_eq_affineCombination`, `convexCombination_single`, `convexComboPair_eq_lineMap`, `convexCombination_eq_sum`	5
Total	7

AddTorsor

Definitions

Name	Category	Theorems
`convexCombination` 📖	CompOp	2 math math: `convexCombination_assoc`, `convexCombination_single`
`instConvexSpace` 📖	CompOp	5 math math: `ConvexSpace.ofConvex.coe_convexCombination`, `convexCombination_eq_affineCombination`, `convexCombination_eq_sum`, `instIsConvexMetricSpace`, `convexComboPair_eq_lineMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexCombination_assoc` 📖	mathematical	—	`convexCombination` `StdSimplex.map` `Ring.toSemiring` `StdSimplex` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `StdSimplex.join`	—	`nonempty` `Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` `StdSimplex.total` `Finset.weightedVSubOfPoint_apply` `Finset.sum_congr` `Finsupp.sum_mapDomain_index` `zero_smul` `add_smul` `vadd_vsub` `Finset.smul_sum` `smul_smul` `Finsupp.sum_finset_sum_index` `MulZeroClass.zero_mul` `Finset.sum_const_zero` `Finset.ext` `LT.lt.ne'` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `LE.le.lt_of_ne'` `StdSimplex.nonneg` `MulZeroClass.mul_zero`
`convexCombination_eq_affineCombination` 📖	mathematical	—	`ConvexSpace.convexCombination` `Ring.toSemiring` `ConvexSpace` `instConvexSpace` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Finsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StdSimplex.weights` `Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finsupp` `Finsupp.instFunLike`	—	—
`convexCombination_single` 📖	mathematical	—	`convexCombination` `StdSimplex.single` `Ring.toSemiring`	—	`Finsupp.support_single_ne_zero` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Finset.affineCombination_of_eq_one_of_eq_zero` `Finset.mem_singleton_self` `Finsupp.single_eq_same` `Finsupp.single_eq_of_ne`
`convexComboPair_eq_lineMap` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`convexComboPair` `Ring.toSemiring` `instConvexSpace` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`convexCombination_eq_affineCombination` `Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` `Finset.sum_congr` `Finsupp.sum_add_index` `Finsupp.sum_single_index` `Finset.weightedVSubOfPoint_apply` `zero_smul` `add_smul` `vsub_self` `smul_zero` `add_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexCombination_eq_sum` 📖	mathematical	—	`ConvexSpace.convexCombination` `Ring.toSemiring` `ConvexSpace` `AddTorsor.instConvexSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toAddCommMonoid` `StdSimplex.weights` `Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SMulZeroClass.toSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`AddTorsor.convexCombination_eq_affineCombination` `Finset.affineCombination_eq_linear_combination` `StdSimplex.total` `Finset.sum_congr`

---

← Back to Index