Combination

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

Statistics

Metric	Count
Definitions weightedVSubOfPoint, affineCombination, affineCombinationLineMapWeights, affineCombinationSingleWeights, instAddTorsorForall, weightedVSub, weightedVSubOfPoint, weightedVSubVSubWeights	8
Theorems affineCombinationLineMapWeights_apply_left, affineCombinationLineMapWeights_apply_of_ne, affineCombinationLineMapWeights_apply_right, affineCombinationLineMapWeights_self, affineCombinationSingleWeights_apply_of_ne, affineCombinationSingleWeights_apply_self, affineCombination_affineCombinationLineMapWeights, affineCombination_affineCombinationSingleWeights, affineCombination_apply, affineCombination_apply_const, affineCombination_apply_eq_lineMap_sum, affineCombination_congr, affineCombination_eq_linear_combination, affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, affineCombination_filter_of_ne, affineCombination_indicator_subset, affineCombination_linear, affineCombination_map, affineCombination_of_eq_one_of_eq_zero, affineCombination_sdiff_sub, affineCombination_subtype_eq_filter, affineCombination_vsub, attach_affineCombination_coe, attach_affineCombination_of_injective, eq_affineCombination_subset_iff_eq_affineCombination_subtype, eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype, eq_weightedVSub_subset_iff_eq_weightedVSub_subtype, map_affineCombination, sum_affineCombinationLineMapWeights, sum_affineCombinationSingleWeights, sum_smul_const_vsub_eq_neg_weightedVSub, sum_smul_const_vsub_eq_sub_weightedVSubOfPoint, sum_smul_const_vsub_eq_vsub_affineCombination, sum_smul_vsub_const_eq_affineCombination_vsub, sum_smul_vsub_const_eq_weightedVSub, sum_smul_vsub_const_eq_weightedVSubOfPoint_sub, sum_smul_vsub_eq_affineCombination_vsub, sum_smul_vsub_eq_weightedVSubOfPoint_sub, sum_smul_vsub_eq_weightedVSub_sub, sum_weightedVSubVSubWeights, univ_fin2, weightedVSubOfPoint_apply, weightedVSubOfPoint_apply_const, weightedVSubOfPoint_congr, weightedVSubOfPoint_const_smul, weightedVSubOfPoint_eq_of_sum_eq_zero, weightedVSubOfPoint_eq_of_weights_eq, weightedVSubOfPoint_erase, weightedVSubOfPoint_filter_of_ne, weightedVSubOfPoint_indicator_subset, weightedVSubOfPoint_insert, weightedVSubOfPoint_map, weightedVSubOfPoint_sdiff, weightedVSubOfPoint_sdiff_sub, weightedVSubOfPoint_smul, weightedVSubOfPoint_subtype_eq_filter, weightedVSubOfPoint_vadd, weightedVSubOfPoint_vadd_eq_of_sum_eq_one, weightedVSubVSubWeights_apply_left, weightedVSubVSubWeights_apply_of_ne, weightedVSubVSubWeights_apply_right, weightedVSubVSubWeights_self, weightedVSub_apply, weightedVSub_apply_const, weightedVSub_congr, weightedVSub_const_smul, weightedVSub_empty, weightedVSub_eq_linear_combination, weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, weightedVSub_filter_of_ne, weightedVSub_indicator_subset, weightedVSub_map, weightedVSub_sdiff, weightedVSub_sdiff_sub, weightedVSub_smul, weightedVSub_subtype_eq_filter, weightedVSub_vadd, weightedVSub_vadd_affineCombination, weightedVSub_weightedVSubVSubWeights, affineCombination_mem_affineSpan, affineCombination_mem_affineSpan_image, affineCombination_mem_affineSpan_of_nonempty, affineSpan_eq_affineSpan_lineMap_units, eq_affineCombination_of_mem_affineSpan, eq_affineCombination_of_mem_affineSpan_image, eq_affineCombination_of_mem_affineSpan_of_fintype, mem_affineSpan_iff_eq_affineCombination, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd, mem_vectorSpan_iff_eq_weightedVSub, weightedVSub_mem_vectorSpan	91
Total	99

AffineMap

Definitions

Name	Category	Theorems
weightedVSubOfPoint 📖	CompOp	—

Finset

Definitions

Name	Category	Theorems
affineCombination 📖	CompOp	83 math math: Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, Affine.Simplex.affineCombination_mem_closedInterior_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, affineCombination_vsub, affineCombination_affineCombinationSingleWeights, affineCombination_apply_eq_lineMap_sum, centroid_eq_affineCombination_fintype, affineCombination_sdiff_sub, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff, Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff, AffineIndependent.affineCombination_eq_iff_eq, affineCombination_apply_const, Affine.Simplex.excenter_eq_affineCombination, affineCombination_mem_affineSpan_pair, Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo, affineCombination_congr, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_eq_linear_combination, sum_smul_const_vsub_eq_vsub_affineCombination, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg, mem_affineSpan_iff_eq_affineCombination, affineCombination_of_eq_one_of_eq_zero, affineCombination_mem_affineSpan, dist_affineCombination_lt_of_strictConvexSpace, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff, attach_affineCombination_coe, eq_affineCombination_of_mem_affineSpan_image, map_affineCombination, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff, affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem, affineCombination_map, eq_affineCombination_of_mem_affineSpan_of_fintype, AffineBasis.coord_apply_combination_of_notMem, affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, affineCombination_indicator_subset, Affine.Simplex.affineCombination_mem_interior_iff, Affine.Simplex.affineCombination_eq_touchpoint_iff, affineCombination_linear, affineCombination_apply, affineCombination_mem_affineSpan_image, affineCombination_affineCombinationLineMapWeights, affineCombination_filter_of_ne, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, eq_affineCombination_of_mem_affineSpan, Affine.Simplex.affineCombination_mem_interior_face_iff_pos, Affine.Simplex.incenter_eq_affineCombination, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg, Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, eq_affineCombination_subset_iff_eq_affineCombination_subtype, affineCombination_mem_convexHull, weightedVSub_vadd_affineCombination, affineCombination_mem_affineSpan_of_nonempty, Affine.Simplex.centroid_eq_affineCombination, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff, Affine.Simplex.affineCombination_touchpointWeights, attach_affineCombination_of_injective, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc, affineCombination_eq_centerMass, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, Affine.Simplex.signedInfDist_affineCombination, EuclideanGeometry.dist_affineCombination, sum_smul_vsub_const_eq_affineCombination_vsub, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff, AffineBasis.affineCombination_coord_eq_self, sum_smul_vsub_eq_affineCombination_vsub, AffineBasis.coord_apply_combination_of_mem, AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, weightedVSub_mem_vectorSpan_pair, Affine.Simplex.affineCombination_mem_setInterior_iff, centroid_def, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, affineCombination_subtype_eq_filter, convexHull_range_eq_exists_affineCombination, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff
affineCombinationLineMapWeights 📖	CompOp	6 math math: affineCombinationLineMapWeights_apply_left, affineCombinationLineMapWeights_apply_right, affineCombination_affineCombinationLineMapWeights, sum_affineCombinationLineMapWeights, affineCombinationLineMapWeights_self, affineCombinationLineMapWeights_apply_of_ne
affineCombinationSingleWeights 📖	CompOp	5 math math: affineCombinationSingleWeights_apply_of_ne, affineCombination_affineCombinationSingleWeights, affineCombinationSingleWeights_apply_self, affineCombinationLineMapWeights_self, sum_affineCombinationSingleWeights
instAddTorsorForall 📖	CompOp	90 math math: Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Affine.Simplex.affineCombination_mem_closedInterior_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, affineCombination_vsub, affineCombination_affineCombinationSingleWeights, affineCombination_apply_eq_lineMap_sum, centroid_eq_affineCombination_fintype, affineCombination_sdiff_sub, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff, Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff, AffineIndependent.affineCombination_eq_iff_eq, affineCombination_apply_const, Affine.Simplex.excenter_eq_affineCombination, affineCombination_mem_affineSpan_pair, Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo, affineCombination_congr, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_eq_linear_combination, sum_smul_const_vsub_eq_vsub_affineCombination, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg, mem_affineSpan_iff_eq_affineCombination, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, affineCombination_of_eq_one_of_eq_zero, affineCombination_mem_affineSpan, dist_affineCombination_lt_of_strictConvexSpace, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff, attach_affineCombination_coe, eq_affineCombination_of_mem_affineSpan_image, map_affineCombination, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff, affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem, AffineBasis.toMatrix_vecMul_coords, affineCombination_map, AffineBasis.det_smul_coords_eq_cramer_coords, eq_affineCombination_of_mem_affineSpan_of_fintype, AffineBasis.coord_apply_combination_of_notMem, affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, affineCombination_indicator_subset, Affine.Simplex.affineCombination_mem_interior_iff, Affine.Simplex.affineCombination_eq_touchpoint_iff, affineCombination_linear, affineCombination_apply, affineCombination_mem_affineSpan_image, affineCombination_affineCombinationLineMapWeights, affineCombination_filter_of_ne, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, eq_affineCombination_of_mem_affineSpan, Affine.Simplex.affineCombination_mem_interior_face_iff_pos, AffineBasis.toMatrix_inv_vecMul_toMatrix, Affine.Simplex.incenter_eq_affineCombination, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, AffineBasis.coords_apply, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg, Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, eq_affineCombination_subset_iff_eq_affineCombination_subtype, affineCombination_mem_convexHull, weightedVSub_vadd_affineCombination, affineCombination_mem_affineSpan_of_nonempty, Affine.Simplex.centroid_eq_affineCombination, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff, Affine.Simplex.affineCombination_touchpointWeights, mem_fintypeAffineCoords_iff_sum, attach_affineCombination_of_injective, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc, affineCombination_eq_centerMass, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, Affine.Simplex.signedInfDist_affineCombination, EuclideanGeometry.dist_affineCombination, sum_smul_vsub_const_eq_affineCombination_vsub, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff, AffineBasis.affineCombination_coord_eq_self, sum_smul_vsub_eq_affineCombination_vsub, AffineBasis.coord_apply_combination_of_mem, AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, weightedVSub_mem_vectorSpan_pair, Affine.Simplex.affineCombination_mem_setInterior_iff, centroid_def, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, affineCombination_subtype_eq_filter, convexHull_range_eq_exists_affineCombination, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff
weightedVSub 📖	CompOp	29 math math: weightedVSub_sdiff, affineCombination_vsub, affineCombination_sdiff_sub, weightedVSub_apply_const, weightedVSub_map, mem_vectorSpan_iff_eq_weightedVSub, weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, weightedVSub_empty, weightedVSub_weightedVSubVSubWeights, weightedVSub_smul, weightedVSub_const_smul, sum_smul_const_vsub_eq_neg_weightedVSub, affineCombination_linear, weightedVSub_filter_of_ne, weightedVSub_vadd, weightedVSub_mem_vectorSpan, EuclideanGeometry.inner_weightedVSub, weightedVSub_congr, eq_weightedVSub_subset_iff_eq_weightedVSub_subtype, weightedVSub_eq_linear_combination, weightedVSub_vadd_affineCombination, weightedVSub_apply, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, sum_smul_vsub_const_eq_weightedVSub, weightedVSub_subtype_eq_filter, weightedVSub_sdiff_sub, weightedVSub_indicator_subset, weightedVSub_mem_vectorSpan_pair, sum_smul_vsub_eq_weightedVSub_sub
weightedVSubOfPoint 📖	CompOp	25 math math: weightedVSubOfPoint_map, weightedVSubOfPoint_apply, weightedVSubOfPoint_insert, weightedVSubOfPoint_congr, weightedVSubOfPoint_indicator_subset, sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_vadd, weightedVSubOfPoint_filter_of_ne, weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, weightedVSubOfPoint_sdiff, eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype, affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, affineCombination_apply, weightedVSubOfPoint_smul, weightedVSubOfPoint_vadd_eq_of_sum_eq_one, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd, weightedVSubOfPoint_apply_const, weightedVSubOfPoint_eq_of_weights_eq, weightedVSubOfPoint_eq_of_sum_eq_zero, weightedVSubOfPoint_const_smul, sum_smul_const_vsub_eq_sub_weightedVSubOfPoint, weightedVSubOfPoint_erase, sum_smul_vsub_const_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_subtype_eq_filter, weightedVSubOfPoint_sdiff_sub
weightedVSubVSubWeights 📖	CompOp	6 math math: weightedVSubVSubWeights_apply_of_ne, weightedVSub_weightedVSubVSubWeights, weightedVSubVSubWeights_self, weightedVSubVSubWeights_apply_right, weightedVSubVSubWeights_apply_left, sum_weightedVSubVSubWeights

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineCombinationLineMapWeights_apply_left 📖	mathematical	—	affineCombinationLineMapWeights SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	weightedVSubVSubWeights_apply_right mul_neg mul_one affineCombinationSingleWeights_apply_self sub_eq_neg_add
affineCombinationLineMapWeights_apply_of_ne 📖	mathematical	—	affineCombinationLineMapWeights MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	weightedVSubVSubWeights_apply_of_ne MulZeroClass.mul_zero affineCombinationSingleWeights_apply_of_ne add_zero
affineCombinationLineMapWeights_apply_right 📖	mathematical	—	affineCombinationLineMapWeights	—	weightedVSubVSubWeights_apply_left mul_one affineCombinationSingleWeights_apply_of_ne add_zero
affineCombinationLineMapWeights_self 📖	mathematical	—	affineCombinationLineMapWeights affineCombinationSingleWeights	—	weightedVSubVSubWeights_self smul_zero zero_add
affineCombinationSingleWeights_apply_of_ne 📖	mathematical	—	affineCombinationSingleWeights MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Pi.single_eq_of_ne
affineCombinationSingleWeights_apply_self 📖	mathematical	—	affineCombinationSingleWeights AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Pi.single_eq_same
affineCombination_affineCombinationLineMapWeights 📖	mathematical	Finset instMembership	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination affineCombinationLineMapWeights addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.lineMap	—	affineCombinationLineMapWeights.eq_1 weightedVSub_vadd_affineCombination weightedVSub_const_smul affineCombination_affineCombinationSingleWeights weightedVSub_weightedVSubVSubWeights AffineMap.lineMap_apply
affineCombination_affineCombinationSingleWeights 📖	mathematical	Finset instMembership	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination affineCombinationSingleWeights	—	affineCombination_of_eq_one_of_eq_zero affineCombinationSingleWeights_apply_self affineCombinationSingleWeights_apply_of_ne
affineCombination_apply 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid LinearMap.instFunLike weightedVSubOfPoint AddTorsor.nonempty	—	—
affineCombination_apply_const 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination	—	AddTorsor.nonempty affineCombination_apply weightedVSubOfPoint_apply_const one_smul vsub_vadd
affineCombination_apply_eq_lineMap_sum 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination addGroupIsAddTorsor AddGroupWithOne.toAddGroup AffineMap.lineMap Finset instInter	—	affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one weightedVSubOfPoint_apply sum_inter_add_sum_diff AffineMap.lineMap_apply vadd_right_cancel_iff sum_smul sum_congr vsub_self smul_zero sum_const_zero add_zero
affineCombination_congr 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination	—	AddTorsor.nonempty weightedVSubOfPoint_congr
affineCombination_eq_linear_combination 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike affineCombination AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one weightedVSubOfPoint_apply sum_congr sub_zero add_zero
affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finset instMembership NegZeroClass.toNeg Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AffineMap Pi.addCommGroup NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instAddTorsorForall AffineMap.instFunLike affineCombination filter	—	vsub_eq_zero_iff_eq affineCombination_sdiff_sub singleton_subset_iff sdiff_singleton_eq_erase filter_ne' affineCombination_of_eq_one_of_eq_zero mem_singleton_self neg_neg instIsEmptyFalse
affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid LinearMap.instFunLike weightedVSubOfPoint	—	weightedVSubOfPoint_vadd_eq_of_sum_eq_one
affineCombination_filter_of_ne 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination filter	—	AddTorsor.nonempty affineCombination_apply weightedVSubOfPoint_filter_of_ne
affineCombination_indicator_subset 📖	mathematical	Finset instHasSubset	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination Set.indicator MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SetLike.coe instSetLike	—	AddTorsor.nonempty affineCombination_apply weightedVSubOfPoint_indicator_subset
affineCombination_linear 📖	mathematical	—	AffineMap.linear Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall affineCombination weightedVSub	—	—
affineCombination_map 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination map Function.Embedding Function.instFunLikeEmbedding	—	AddTorsor.nonempty weightedVSubOfPoint_map
affineCombination_of_eq_one_of_eq_zero 📖	mathematical	Finset instMembership AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination	—	sum_eq_single affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one weightedVSubOfPoint_apply sum_eq_zero vsub_self smul_zero zero_smul zero_vadd
affineCombination_sdiff_sub 📖	mathematical	Finset instHasSubset	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination instSDiff Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid LinearMap.instFunLike weightedVSub	—	AddTorsor.nonempty vadd_vsub_vadd_cancel_right weightedVSub_sdiff_sub
affineCombination_subtype_eq_filter 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination subtype filter	—	AddTorsor.nonempty affineCombination_apply weightedVSubOfPoint_subtype_eq_filter
affineCombination_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid LinearMap.instFunLike weightedVSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	AffineMap.linearMap_vsub affineCombination_linear vsub_eq_sub
attach_affineCombination_coe 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Finset instMembership Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination attach SetLike.instMembership instSetLike	—	attach_affineCombination_of_injective Subtype.coe_injective univ_eq_attach attach_image_val
attach_affineCombination_of_injective 📖	mathematical	Finset SetLike.instMembership instSetLike	DFunLike.coe AffineMap Pi.addCommGroup instMembership Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination attach image univ Subtype.fintype	—	weightedVSubOfPoint_apply sum_congr sum_image coe_attach
eq_affineCombination_subset_iff_eq_affineCombination_subtype 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset instSetLike sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination Set.Elem Set.instMembership	—	AddTorsor.nonempty eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset instSetLike sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint Set.Elem Set.instMembership	—	weightedVSubOfPoint_apply sum_subtype_of_mem map_subtype_subset sum_congr sum_map Subtype.coe_eta dite_smul zero_smul
eq_weightedVSub_subset_iff_eq_weightedVSub_subtype 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset instSetLike sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub Set.Elem Set.instMembership	—	eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
map_affineCombination 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap AffineMap.instFunLike Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall affineCombination	—	AddTorsor.nonempty affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one weightedVSubOfPoint_vadd_eq_of_sum_eq_one weightedVSubOfPoint_apply AffineMap.map_vadd map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sum_congr MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass AffineMap.linearMap_vsub
sum_affineCombinationLineMapWeights 📖	mathematical	Finset instMembership	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing affineCombinationLineMapWeights AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	sum_congr sum_add_distrib sum_weightedVSubVSubWeights MulZeroClass.mul_zero sum_affineCombinationSingleWeights zero_add
sum_affineCombinationSingleWeights 📖	mathematical	Finset instMembership	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing affineCombinationSingleWeights AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombinationSingleWeights_apply_self sum_eq_single_of_mem affineCombinationSingleWeights_apply_of_ne
sum_smul_const_vsub_eq_neg_weightedVSub 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub	—	sum_smul_vsub_eq_weightedVSub_sub weightedVSub_apply_const zero_sub
sum_smul_const_vsub_eq_sub_weightedVSubOfPoint 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub SubNegMonoid.toSub NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	sum_smul_vsub_eq_weightedVSubOfPoint_sub weightedVSubOfPoint_apply_const
sum_smul_const_vsub_eq_vsub_affineCombination 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination	—	sum_smul_vsub_eq_affineCombination_vsub affineCombination_apply_const
sum_smul_vsub_const_eq_affineCombination_vsub 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination	—	sum_smul_vsub_eq_affineCombination_vsub affineCombination_apply_const
sum_smul_vsub_const_eq_weightedVSub 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub	—	sum_smul_vsub_eq_weightedVSub_sub weightedVSub_apply_const sub_zero
sum_smul_vsub_const_eq_weightedVSubOfPoint_sub 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub SubNegMonoid.toSub DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	sum_smul_vsub_eq_weightedVSubOfPoint_sub weightedVSubOfPoint_apply_const
sum_smul_vsub_eq_affineCombination_vsub 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule instAddTorsorForall AffineMap.instFunLike affineCombination	—	AddTorsor.nonempty vadd_vsub_vadd_cancel_right sum_smul_vsub_eq_weightedVSubOfPoint_sub
sum_smul_vsub_eq_weightedVSubOfPoint_sub 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub SubNegMonoid.toSub DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	weightedVSubOfPoint_apply sum_congr vsub_sub_vsub_cancel_right
sum_smul_vsub_eq_weightedVSub_sub 📖	mathematical	—	sum AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction VSub.vsub AddTorsor.toVSub SubNegMonoid.toSub DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub	—	sum_smul_vsub_eq_weightedVSubOfPoint_sub
sum_weightedVSubVSubWeights 📖	mathematical	Finset instMembership	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing weightedVSubVSubWeights MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	sum_congr sum_sub_distrib sum_affineCombinationSingleWeights sub_self
univ_fin2 📖	mathematical	—	univ Fin.fintype Finset instInsert instSingleton	—	—
weightedVSubOfPoint_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction VSub.vsub AddTorsor.toVSub	—	LinearMap.sum_apply sum_congr
weightedVSubOfPoint_apply_const 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction sum VSub.vsub AddTorsor.toVSub	—	weightedVSubOfPoint_apply sum_smul
weightedVSubOfPoint_congr 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	weightedVSubOfPoint_apply sum_congr
weightedVSubOfPoint_const_smul 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass instDistribSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	weightedVSubOfPoint_apply smul_sum sum_congr smul_smul
weightedVSubOfPoint_eq_of_sum_eq_zero 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	eq_of_sub_eq_zero weightedVSubOfPoint_apply sum_sub_distrib smul_sub vsub_sub_vsub_cancel_left sum_smul zero_smul
weightedVSubOfPoint_eq_of_weights_eq 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	weightedVSubOfPoint_apply eq_or_ne vsub_self smul_zero
weightedVSubOfPoint_erase 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint erase	—	weightedVSubOfPoint_apply sum_erase vsub_self smul_zero
weightedVSubOfPoint_filter_of_ne 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint filter	—	weightedVSubOfPoint_apply sum_filter_of_ne zero_smul
weightedVSubOfPoint_indicator_subset 📖	mathematical	Finset instHasSubset	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint Set.indicator MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SetLike.coe instSetLike	—	weightedVSubOfPoint_apply sum_indicator_subset_of_eq_zero zero_smul
weightedVSubOfPoint_insert 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint Finset instInsert	—	weightedVSubOfPoint_apply sum_insert_zero vsub_self smul_zero
weightedVSubOfPoint_map 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint map Function.Embedding Function.instFunLikeEmbedding	—	weightedVSubOfPoint_apply sum_map
weightedVSubOfPoint_sdiff 📖	mathematical	Finset instHasSubset	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint instSDiff	—	weightedVSubOfPoint_apply sum_sdiff
weightedVSubOfPoint_sdiff_sub 📖	mathematical	Finset instHasSubset	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint instSDiff Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_neg_eq_add weightedVSubOfPoint_sdiff
weightedVSubOfPoint_smul 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint addGroupIsAddTorsor AddCommGroup.toAddGroup Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	weightedVSubOfPoint_apply sum_congr smul_sub sum_sub_distrib smul_sum SMulCommClass.smul_comm smul_inv_smul
weightedVSubOfPoint_subtype_eq_filter 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint subtype filter	—	weightedVSubOfPoint_apply sum_subtype_eq_sum_filter
weightedVSubOfPoint_vadd 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint HVAdd.hVAdd instHVAdd Function.hasVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	weightedVSubOfPoint_apply sum_congr vadd_vsub_assoc smul_add vsub_vadd_eq_vsub_sub sub_neg_eq_add add_comm
weightedVSubOfPoint_vadd_eq_of_sum_eq_one 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSubOfPoint	—	weightedVSubOfPoint_apply vsub_eq_zero_iff_eq vadd_vsub_assoc vsub_vadd_eq_vsub_sub add_sub_assoc add_comm sum_sub_distrib smul_sub vsub_sub_vsub_cancel_left sum_smul one_smul vsub_add_vsub_cancel vsub_self
weightedVSubVSubWeights_apply_left 📖	mathematical	—	weightedVSubVSubWeights AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombinationSingleWeights_apply_self affineCombinationSingleWeights_apply_of_ne sub_zero
weightedVSubVSubWeights_apply_of_ne 📖	mathematical	—	weightedVSubVSubWeights MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	affineCombinationSingleWeights_apply_of_ne sub_self
weightedVSubVSubWeights_apply_right 📖	mathematical	—	weightedVSubVSubWeights NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombinationSingleWeights_apply_of_ne affineCombinationSingleWeights_apply_self zero_sub
weightedVSubVSubWeights_self 📖	mathematical	—	weightedVSubVSubWeights Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_self
weightedVSub_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction VSub.vsub AddTorsor.toVSub AddTorsor.nonempty	—	AddTorsor.nonempty weightedVSubOfPoint_apply
weightedVSub_apply_const 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	weightedVSub.eq_1 weightedVSubOfPoint_apply_const zero_smul
weightedVSub_congr 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub	—	weightedVSubOfPoint_congr
weightedVSub_const_smul 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass instDistribSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	weightedVSubOfPoint_const_smul
weightedVSub_empty 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub Finset instEmptyCollection NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	weightedVSub_apply
weightedVSub_eq_linear_combination 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub addGroupIsAddTorsor AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	AddTorsor.nonempty weightedVSub_apply sum_congr smul_sub sum_sub_distrib zero_smul sub_zero
weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub weightedVSubOfPoint	—	weightedVSubOfPoint_eq_of_sum_eq_zero
weightedVSub_filter_of_ne 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub filter	—	weightedVSubOfPoint_filter_of_ne
weightedVSub_indicator_subset 📖	mathematical	Finset instHasSubset	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub Set.indicator MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SetLike.coe instSetLike	—	weightedVSubOfPoint_indicator_subset
weightedVSub_map 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub map Function.Embedding Function.instFunLikeEmbedding	—	weightedVSubOfPoint_map
weightedVSub_sdiff 📖	mathematical	Finset instHasSubset	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub instSDiff	—	weightedVSubOfPoint_sdiff
weightedVSub_sdiff_sub 📖	mathematical	Finset instHasSubset	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub instSDiff Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	weightedVSubOfPoint_sdiff_sub
weightedVSub_smul 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub addGroupIsAddTorsor AddCommGroup.toAddGroup Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	—	weightedVSub.eq_1 weightedVSubOfPoint_smul weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero
weightedVSub_subtype_eq_filter 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub subtype filter	—	weightedVSubOfPoint_subtype_eq_filter
weightedVSub_vadd 📖	mathematical	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub HVAdd.hVAdd instHVAdd Function.hasVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	weightedVSub.eq_1 weightedVSubOfPoint_vadd weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero
weightedVSub_vadd_affineCombination 📖	mathematical	—	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub AffineMap Pi.addCommGroup Ring.toAddCommGroup NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instAddTorsorForall AffineMap.instFunLike affineCombination Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	vadd_eq_add AffineMap.map_vadd affineCombination_linear
weightedVSub_weightedVSubVSubWeights 📖	mathematical	Finset instMembership	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike weightedVSub weightedVSubVSubWeights VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	weightedVSubVSubWeights.eq_1 affineCombination_vsub affineCombination_affineCombinationSingleWeights

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineCombination_mem_affineSpan 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	one_ne_zero NeZero.one Finset.nonempty_of_sum_ne_zero Finset.sum_congr Finset.sum_update_of_mem Finset.sum_const_zero add_zero Finset.affineCombination_of_eq_one_of_eq_zero Function.update_self Function.update_of_ne direction_affineSpan Finset.affineCombination_vsub weightedVSub_mem_vectorSpan Finset.sum_sub_distrib sub_self vsub_vadd AffineSubspace.vadd_mem_of_mem_direction mem_affineSpan Set.mem_range_self
affineCombination_mem_affineSpan_image 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.image DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	Set.image_eq_range Finset.sum_sdiff right_eq_add AddRightCancelSemigroup.toIsRightCancelAdd Finset.sum_eq_zero Finset.affineCombination_subtype_eq_filter Finset.affineCombination_indicator_subset Finset.filter_subset Finset.affineCombination_congr Finset.coe_filter Set.indicator_apply affineCombination_mem_affineSpan Finset.sum_subtype_eq_sum_filter
affineCombination_mem_affineSpan_of_nonempty 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	subsingleton_or_nontrivial Module.subsingleton affineSpan_eq_top_iff_nonempty_of_subsingleton AddTorsor.subsingleton_iff Set.range_nonempty affineCombination_mem_affineSpan
affineSpan_eq_affineSpan_lineMap_units 📖	mathematical	Set Set.instMembership	affineSpan Set.range Set.Elem DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Subtype.range_coe_subtype le_antisymm mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd AffineMap.lineMap_same Finset.weightedVSubOfPoint_apply Finset.sum_congr AffineMap.lineMap_vsub_left smul_smul Units.inv_mul_cancel_right
eq_affineCombination_of_mem_affineSpan 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	Set.range_nonempty_iff_nonempty affineSpan_nonempty mem_affineSpan Set.mem_range_self AffineSubspace.vsub_mem_direction mem_vectorSpan_iff_eq_weightedVSub direction_affineSpan Finset.sum_indicator_subset Finset.subset_insert Finset.weightedVSub_indicator_subset Finset.sum_update_of_mem Finset.mem_insert_self Finset.sum_congr Finset.sum_const_zero add_zero Finset.affineCombination_of_eq_one_of_eq_zero Function.update_self Function.update_of_ne Finset.sum_add_distrib add_comm Finset.weightedVSub_vadd_affineCombination vsub_vadd
eq_affineCombination_of_mem_affineSpan_image 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.image	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	eq_affineCombination_of_mem_affineSpan Set.image_eq_range Finset.coe_map Set.image_congr Subtype.coe_preimage_self Finset.sum_congr Finset.sum_map Subtype.coe_eta Finset.affineCombination_map Finset.affineCombination_congr
eq_affineCombination_of_mem_affineSpan_of_fintype 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	eq_affineCombination_of_mem_affineSpan Finset.sum_congr Set.indicator_apply Fintype.sum_extend_by_zero Finset.affineCombination_indicator_subset Finset.subset_univ
mem_affineSpan_iff_eq_affineCombination 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination	—	eq_affineCombination_of_mem_affineSpan affineCombination_mem_affineSpan
mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike Finset.weightedVSubOfPoint	—	eq_affineCombination_of_mem_affineSpan Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one Finset.sum_congr Finset.insert_eq_of_mem Finset.sum_update_of_mem sub_add_cancel Finset.sum_insert Finset.sum_update_of_notMem Function.update_self Finset.erase_eq_of_notMem Function.update_of_ne Finset.weightedVSubOfPoint_eq_of_weights_eq Finset.weightedVSubOfPoint_insert affineCombination_mem_affineSpan
mem_vectorSpan_iff_eq_weightedVSub 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan Set.range Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike Finset.weightedVSub	—	isEmpty_or_nonempty Set.range_eq_empty vectorSpan_empty Submodule.mem_bot Finset.weightedVSub_empty AddTorsor.nonempty vectorSpan_range_eq_span_range_vsub_right Set.image_univ Finsupp.mem_span_image_iff_linearCombination Finset.sum_congr Finset.sum_sub_distrib Finset.sum_update_of_mem Finset.mem_insert_self Finset.sum_insert_of_eq_zero_if_notMem Finsupp.notMem_support_iff Finset.sum_const_zero add_zero sub_self smul_zero vsub_self Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero Finset.weightedVSubOfPoint_apply Finsupp.linearCombination_apply Finset.sum_insert_zero Function.update_of_ne sub_zero weightedVSub_mem_vectorSpan
weightedVSub_mem_vectorSpan 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan Set.range DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike Finset.weightedVSub	—	isEmpty_or_nonempty Finset.eq_empty_of_isEmpty Finset.weightedVSub_empty AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass vectorSpan_range_eq_span_range_vsub_right Set.image_univ Finsupp.mem_span_image_iff_linearCombination Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero Finset.weightedVSubOfPoint_apply Set.mem_of_indicator_ne_zero Set.subset_univ Finsupp.linearCombination_apply Finsupp.onFinset_sum zero_smul Finset.sum_congr Set.indicator_apply

---

← Back to Index