Centroid

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean

Statistics

Metric	Count
Definitions centroid, faceOppositeCentroid, medial, median	4
Theorems affineIndependent_points_update_centroid, affineSpan_range_medial, centroid_eq_affineCombination, centroid_eq_iff, centroid_eq_of_range_eq, centroid_eq_smul_sum_vsub_vadd, centroid_eq_smul_vsub_vadd_point, centroid_map, centroid_mem_affineSpan, centroid_mem_median, centroid_notMem_affineSpan_of_ne_univ, centroid_reindex, centroid_restrict, centroid_vsub_eq, centroid_vsub_faceOppositeCentroid_eq_smul_vsub, centroid_vsub_point_eq_smul_vsub, centroid_weighted_vsub_eq_zero, eq_centroid_iff_sum_vsub_eq_zero, eq_centroid_of_forall_mem_median, faceOppositeCentroid_eq_affineCombination, faceOppositeCentroid_eq_smul_vsub_vadd_point, faceOppositeCentroid_eq_sum_vsub_vadd, faceOppositeCentroid_map, faceOppositeCentroid_mem_affineSpan_face, faceOppositeCentroid_mem_median, faceOppositeCentroid_reindex, faceOppositeCentroid_restrict, faceOppositeCentroid_vsub_centroid_eq_smul_vsub, faceOppositeCentroid_vsub_faceOppositeCentroid, faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, faceOppositeCentroid_vsub_point_eq_smul_vsub, face_centroid_eq_centroid, face_centroid_eq_iff, medial_map, medial_points, medial_reindex, medial_restrict, median_eq_line_point_centroid, median_map, median_reindex, median_restrict, point_mem_median, point_vsub_centroid_eq_smul_vsub, point_vsub_faceOppositeCentroid_eq_smul_sum_vsub, point_vsub_faceOppositeCentroid_eq_smul_vsub, smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point, smul_centroid_vsub_point_eq_sum_vsub, smul_faceOppositeCentroid_vsub_point_eq_sum_vsub, univ_centroid_eq	49
Total	53

Affine.Simplex

Definitions

Name	Category	Theorems
centroid 📖	CompOp	31 math math: smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point, dist_point_faceOppositeCentroid, centroid_eq_smul_sum_vsub_vadd, Affine.Triangle.dist_point_faceOppositeCentroid, median_eq_line_point_centroid, univ_centroid_eq, affineIndependent_points_update_centroid, point_vsub_faceOppositeCentroid_eq_smul_vsub, centroid_weighted_vsub_eq_zero, centroid_map, centroid_notMem_affineSpan_of_ne_univ, dist_point_centroid, faceOppositeCentroid_vsub_point_eq_smul_vsub, centroid_eq_smul_vsub_vadd_point, centroid_vsub_faceOppositeCentroid_eq_smul_vsub, centroid_restrict, eq_centroid_iff_sum_vsub_eq_zero, collinear_point_centroid_faceOppositeCentroid, eq_centroid_of_forall_mem_median, centroid_eq_affineCombination, smul_centroid_vsub_point_eq_sum_vsub, point_vsub_centroid_eq_smul_vsub, centroid_mem_median, faceOppositeCentroid_eq_smul_vsub_vadd_point, faceOppositeCentroid_vsub_centroid_eq_smul_vsub, centroid_reindex, ninePointCircle_center, centroid_mem_affineSpan, centroid_vsub_point_eq_smul_vsub, centroid_vsub_eq, Affine.Triangle.dist_point_centroid
faceOppositeCentroid 📖	CompOp	29 math math: faceOppositeCentroid_mem_affineSpan_face, faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point, faceOppositeCentroid_restrict, dist_point_faceOppositeCentroid, Affine.Triangle.dist_point_faceOppositeCentroid, point_vsub_faceOppositeCentroid_eq_smul_vsub, smul_faceOppositeCentroid_vsub_point_eq_sum_vsub, dist_point_centroid, point_vsub_faceOppositeCentroid_eq_smul_sum_vsub, faceOppositeCentroid_vsub_point_eq_smul_vsub, faceOppositeCentroid_eq_sum_vsub_vadd, centroid_eq_smul_vsub_vadd_point, centroid_vsub_faceOppositeCentroid_eq_smul_vsub, faceOppositeCentroid_reindex, midpoint_faceOppositeCentroid_eulerPoint, medial_points, collinear_point_centroid_faceOppositeCentroid, faceOppositeCentroid_mem_median, faceOppositeCentroid_mem_ninePointCircle, point_vsub_centroid_eq_smul_vsub, faceOppositeCentroid_map, faceOppositeCentroid_eq_smul_vsub_vadd_point, faceOppositeCentroid_vsub_centroid_eq_smul_vsub, isDiameter_ninePointCircle, faceOppositeCentroid_vsub_faceOppositeCentroid, faceOppositeCentroid_eq_affineCombination, centroid_vsub_point_eq_smul_vsub, Affine.Triangle.dist_point_centroid
medial 📖	CompOp	6 math math: medial_reindex, medial_restrict, ninePointCircle_eq_circumsphere_medial, medial_points, affineSpan_range_medial, medial_map
median 📖	CompOp	7 math math: point_mem_median, median_eq_line_point_centroid, median_reindex, median_map, median_restrict, faceOppositeCentroid_mem_median, centroid_mem_median

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineIndependent_points_update_centroid 📖	mathematical	—	AffineIndependent DivisionRing.toRing Function.update points centroid	—	centroid_notMem_affineSpan_of_ne_univ AffineIndependent.affineIndependent_update_of_notMem_affineSpan independent
affineSpan_range_medial 📖	mathematical	—	affineSpan DivisionRing.toRing Set.range points medial	—	mem_affineSpan Set.mem_of_mem_of_subset faceOppositeCentroid_mem_affineSpan_face affineSpan_mono range_faceOpposite_points Set.preimage_range AffineSubspace.eq_iff_direction_eq_of_mem direction_affineSpan Set.ext neg_vsub_eq_vsub_rev faceOppositeCentroid_vsub_faceOppositeCentroid inv_neg neg_smul Submodule.span_smul_eq_of_isUnit
centroid_eq_affineCombination 📖	mathematical	—	centroid DFunLike.coe AffineMap DivisionRing.toRing Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Finset.centroidWeights	—	—
centroid_eq_iff 📖	mathematical	Finset.card	Finset.centroid points DivisionRing.toRing	—	affineIndependent_iff_indicator_eq_of_affineCombination_eq independent Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one Finset.centroid_eq_affineCombination_fintype Finset.ext Nat.cast_one Nat.cast_zero Nat.cast_add Set.indicator_of_mem Set.indicator_of_notMem Set.indicator_univ Finset.coe_univ
centroid_eq_of_range_eq 📖	mathematical	Set.range points DivisionRing.toRing	Finset.centroid Finset.univ Fin.fintype	—	Finset.centroid_eq_of_inj_on_of_image_eq AffineIndependent.injective DivisionRing.toNontrivial independent Finset.coe_univ Set.image_univ
centroid_eq_smul_sum_vsub_vadd 📖	mathematical	—	centroid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidWithOne.toOne Finset.sum Finset.univ Fin.fintype VSub.vsub AddTorsor.toVSub points	—	centroid_vsub_eq vsub_vadd
centroid_eq_smul_vsub_vadd_point 📖	mathematical	—	centroid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing VSub.vsub AddTorsor.toVSub faceOppositeCentroid points	—	centroid_vsub_point_eq_smul_vsub vsub_vadd
centroid_map 📖	mathematical	DFunLike.coe AffineMap DivisionRing.toRing AffineMap.instFunLike	centroid map	—	centroid.eq_1 map_points centroid_eq_affineCombination Finset.map_affineCombination Finset.sum_centroidWeights_eq_one_of_card_ne_zero Fintype.card_fin Finset.centroid.eq_1
centroid_mem_affineSpan 📖	mathematical	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points centroid	—	centroid_mem_affineSpan_of_card_eq_add_one Finset.card_fin
centroid_mem_median 📖	mathematical	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike median centroid	—	median.eq_1 eq_vadd_iff_vsub_eq centroid_vsub_point_eq_smul_vsub faceOppositeCentroid_vsub_point_eq_smul_vsub smul_smul one_div mul_assoc inv_mul_cancel₀ Nat.cast_one Nat.cast_zero mul_one smul_vsub_vadd_mem_affineSpan_pair
centroid_notMem_affineSpan_of_ne_univ 📖	mathematical	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.image points centroid	—	Set.exists_of_ssubset Finset.sum_centroidWeights_eq_one_of_nonempty AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan independent centroid_eq_affineCombination Fintype.card_fin Nat.cast_add Nat.cast_one one_div Nat.cast_zero
centroid_reindex 📖	mathematical	—	centroid reindex DivisionRing.toRing	—	centroid.eq_1 centroid_eq_affineCombination Fintype.card_fin Fintype.card_eq Finset.univ_map_embedding Equiv.symm_comp_self CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Finset.affineCombination_map
centroid_restrict 📖	mathematical	AffineSubspace DivisionRing.toRing Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	SetLike.instMembership AffineSubspace.instSetLike centroid Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange centroid_map
centroid_vsub_eq 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup centroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidWithOne.toOne Finset.sum Finset.univ Fin.fintype points	—	Finset.centroid_vsub_const Finset.centroid_def Finset.affineCombination_eq_linear_combination Finset.sum_centroidWeights_eq_one_of_nonempty Finset.sum_congr Fintype.card_fin Nat.cast_add Nat.cast_one Finset.smul_sum
centroid_vsub_faceOppositeCentroid_eq_smul_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup centroid faceOppositeCentroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing points	—	point_vsub_centroid_eq_smul_vsub smul_smul inv_mul_cancel₀ NeZero.charZero one_smul
centroid_vsub_point_eq_smul_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup centroid points DivisionRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne faceOppositeCentroid	—	neg_vsub_eq_vsub_rev point_vsub_centroid_eq_smul_vsub neg_smul_neg neg_smul neg_neg
centroid_weighted_vsub_eq_zero 📖	mathematical	—	Finset.sum AddCommGroup.toAddCommMonoid Finset.univ Fin.fintype VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup points DivisionRing.toRing centroid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	centroid_vsub_eq smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors DivisionRing.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero inv_ne_zero Nat.cast_one Nat.cast_zero vsub_self
eq_centroid_iff_sum_vsub_eq_zero 📖	mathematical	—	centroid Finset.sum AddCommGroup.toAddCommMonoid Finset.univ Fin.fintype VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup points DivisionRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	centroid_weighted_vsub_eq_zero vsub_eq_zero_iff_eq Finset.sum_congr vsub_sub_vsub_cancel_right Nat.cast_one Nat.cast_smul_eq_nsmul Finset.sum_const Fintype.card_fin zero_sub Finset.sum_sub_distrib smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors DivisionRing.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Nat.cast_zero
eq_centroid_of_forall_mem_median 📖	mathematical	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike median	centroid	—	vsub_eq_zero_iff_eq vsub_vadd affineIndependent_points_update_centroid affineIndependent_iff_linearIndependent_vsub LinearIndependent.comp Finset.card_compl Fintype.card_fin Finset.card_singleton add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finset.one_lt_card_iff LinearIndependent.disjoint_span_image Submodule.disjoint_def
faceOppositeCentroid_eq_affineCombination 📖	mathematical	—	faceOppositeCentroid DFunLike.coe AffineMap DivisionRing.toRing Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton points InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Finset.card_compl Fintype.card_fin Finset.card_singleton add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid face_centroid_eq_centroid Finset.centroid_def Finset.centroidWeights_eq_const
faceOppositeCentroid_eq_smul_vsub_vadd_point 📖	mathematical	—	faceOppositeCentroid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing VSub.vsub AddTorsor.toVSub centroid points	—	centroid_vsub_point_eq_smul_vsub eq_vadd_iff_vsub_eq smul_smul inv_mul_cancel₀ NeZero.charZero one_smul
faceOppositeCentroid_eq_sum_vsub_vadd 📖	mathematical	—	faceOppositeCentroid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Finset.sum Finset.univ Fin.fintype VSub.vsub AddTorsor.toVSub points	—	faceOppositeCentroid_vsub_point_eq_smul_sum_vsub vsub_vadd
faceOppositeCentroid_map 📖	mathematical	DFunLike.coe AffineMap DivisionRing.toRing AffineMap.instFunLike	faceOppositeCentroid map	—	centroid_eq_affineCombination Finset.map_affineCombination Finset.sum_centroidWeights_eq_one_of_card_ne_zero Fintype.card_fin
faceOppositeCentroid_mem_affineSpan_face 📖	mathematical	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite faceOppositeCentroid	—	centroid_mem_affineSpan
faceOppositeCentroid_mem_median 📖	mathematical	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike median faceOppositeCentroid	—	—
faceOppositeCentroid_reindex 📖	mathematical	—	faceOppositeCentroid reindex DivisionRing.toRing DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	faceOppositeCentroid.eq_1 centroid_eq_of_range_eq range_faceOpposite_reindex Fintype.card_fin Fintype.card_eq
faceOppositeCentroid_restrict 📖	mathematical	AffineSubspace DivisionRing.toRing Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	SetLike.instMembership AffineSubspace.instSetLike faceOppositeCentroid Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange faceOppositeCentroid_map
faceOppositeCentroid_vsub_centroid_eq_smul_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup faceOppositeCentroid centroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing points	—	centroid_vsub_point_eq_smul_vsub smul_smul inv_mul_cancel₀ NeZero.charZero one_smul
faceOppositeCentroid_vsub_faceOppositeCentroid 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup faceOppositeCentroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing points	—	faceOppositeCentroid_eq_sum_vsub_vadd vadd_vsub_vadd_comm Finset.sum_congr vsub_sub_vsub_cancel_right Finset.sum_sub_distrib smul_sub sub_sub_sub_cancel_left Finset.sum_const Finset.card_univ Fintype.card_fin neg_vsub_eq_vsub_rev sub_eq_add_neg add_smul sub_eq_iff_eq_add one_smul smul_add add_comm Nat.cast_smul_eq_nsmul smul_smul inv_eq_one_div one_div_mul_cancel NeZero.charZero
faceOppositeCentroid_vsub_point_eq_smul_sum_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup faceOppositeCentroid points DivisionRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finset.sum Finset.univ Fin.fintype	—	faceOppositeCentroid_eq_affineCombination Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one Finset.sum_const Finset.card_compl Fintype.card_fin Finset.card_singleton add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid nsmul_eq_mul mul_inv_cancel₀ NeZero.charZero Finset.weightedVSubOfPoint_apply vadd_vsub Finset.sum_compl_add_sum Finset.sum_singleton vsub_self smul_zero add_zero Finset.smul_sum
faceOppositeCentroid_vsub_point_eq_smul_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup faceOppositeCentroid points DivisionRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidWithOne.toOne centroid	—	vsub_sub_vsub_cancel_right faceOppositeCentroid_vsub_point_eq_smul_sum_vsub centroid_vsub_eq sub_smul smul_smul mul_sub add_mul Distrib.rightDistribClass mul_inv_cancel₀ NeZero.charZero Nat.cast_one Nat.cast_zero one_mul
face_centroid_eq_centroid 📖	mathematical	Finset.card	Finset.centroid Finset.univ Fin.fintype points DivisionRing.toRing face	—	Finset.coe_map Finset.coe_univ Set.image_univ Finset.range_orderEmbOfFin Finset.centroid_map
face_centroid_eq_iff 📖	mathematical	Finset.card	Finset.centroid Finset.univ Fin.fintype points DivisionRing.toRing face	—	face_centroid_eq_centroid centroid_eq_iff
medial_map 📖	mathematical	DFunLike.coe AffineMap DivisionRing.toRing AffineMap.instFunLike	medial map	—	ext faceOppositeCentroid_map
medial_points 📖	mathematical	—	points DivisionRing.toRing medial faceOppositeCentroid	—	—
medial_reindex 📖	mathematical	—	medial reindex DivisionRing.toRing	—	ext faceOppositeCentroid_reindex
medial_restrict 📖	mathematical	AffineSubspace DivisionRing.toRing Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	medial Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict affineSpan_range_medial	—	ext Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange affineSpan_range_medial faceOppositeCentroid_restrict
median_eq_line_point_centroid 📖	mathematical	—	median affineSpan DivisionRing.toRing Set Set.instInsert points Set.instSingletonSet centroid	—	affineSpan_pair_le_of_right_mem faceOppositeCentroid_eq_smul_vsub_vadd_point neg_vsub_eq_vsub_rev neg_smul one_smul smul_smul mul_neg_one inv_eq_one_div neg_div smul_vsub_rev_vadd_mem_affineSpan_pair median.eq_1 centroid_mem_median le_antisymm
median_map 📖	mathematical	DFunLike.coe AffineMap DivisionRing.toRing AffineMap.instFunLike	median map AffineSubspace.map	—	faceOppositeCentroid_map AffineSubspace.map_span Set.image_pair
median_reindex 📖	mathematical	—	median reindex DivisionRing.toRing AffineSubspace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	AffineSubspace.ext faceOppositeCentroid_reindex
median_restrict 📖	mathematical	AffineSubspace DivisionRing.toRing Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	AffineSubspace.map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion AffineSubspace.subtype median restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineSubspace.map_span Set.image_congr Set.image_pair faceOppositeCentroid_restrict
point_mem_median 📖	mathematical	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike median points	—	—
point_vsub_centroid_eq_smul_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup points DivisionRing.toRing centroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne faceOppositeCentroid	—	vsub_sub_vsub_cancel_right faceOppositeCentroid_vsub_point_eq_smul_sum_vsub centroid_vsub_eq neg_vsub_eq_vsub_rev sub_smul smul_smul neg_smul mul_sub neg_add_eq_sub sub_eq_iff_eq_add mul_inv_cancel₀ NeZero.charZero one_mul add_mul Distrib.rightDistribClass Nat.cast_one Nat.cast_zero
point_vsub_faceOppositeCentroid_eq_smul_sum_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup points DivisionRing.toRing faceOppositeCentroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finset.sum Finset.univ Fin.fintype	—	neg_vsub_eq_vsub_rev faceOppositeCentroid_vsub_point_eq_smul_sum_vsub neg_smul smul_smul Finset.smul_sum Finset.sum_congr one_smul
point_vsub_faceOppositeCentroid_eq_smul_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup points DivisionRing.toRing faceOppositeCentroid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidWithOne.toOne centroid	—	neg_vsub_eq_vsub_rev faceOppositeCentroid_vsub_point_eq_smul_vsub neg_smul neg_smul_neg neg_neg
smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidWithOne.toOne VSub.vsub AddTorsor.toVSub centroid points faceOppositeCentroid	—	smul_faceOppositeCentroid_vsub_point_eq_sum_vsub smul_centroid_vsub_point_eq_sum_vsub
smul_centroid_vsub_point_eq_sum_vsub 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidWithOne.toOne VSub.vsub AddTorsor.toVSub centroid points Finset.sum Finset.univ Fin.fintype	—	centroid_eq_smul_sum_vsub_vadd vadd_vsub smul_smul mul_inv_cancel₀ Nat.cast_one Nat.cast_zero one_smul
smul_faceOppositeCentroid_vsub_point_eq_sum_vsub 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing VSub.vsub AddTorsor.toVSub faceOppositeCentroid points Finset.sum Finset.univ Fin.fintype	—	faceOppositeCentroid_eq_sum_vsub_vadd vadd_vsub smul_smul mul_inv_cancel₀ NeZero.charZero one_smul
univ_centroid_eq 📖	mathematical	—	Finset.centroid Finset.univ Fin.fintype points DivisionRing.toRing centroid	—	—

---

← Back to Index