Commit 2023-04-07 11:00 b210ed13

View on Github →

feat: port LinearAlgebra.AffineSpace.Combination (#3051)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Combination.lean

added def AffineMap.weightedVSubOfPoint

added def Finset.affineCombination

added def Finset.affineCombinationLineMapWeights

added theorem Finset.affineCombinationLineMapWeights_apply_left

added theorem Finset.affineCombinationLineMapWeights_apply_of_ne

added theorem Finset.affineCombinationLineMapWeights_apply_right

added theorem Finset.affineCombinationLineMapWeights_self

added def Finset.affineCombinationSingleWeights

added theorem Finset.affineCombinationSingleWeights_apply_of_ne

added theorem Finset.affineCombinationSingleWeights_apply_self

added theorem Finset.affineCombination_affineCombinationLineMapWeights

added theorem Finset.affineCombination_affineCombinationSingleWeights

added theorem Finset.affineCombination_apply

added theorem Finset.affineCombination_apply_const

added theorem Finset.affineCombination_congr

added theorem Finset.affineCombination_eq_linear_combination

added theorem Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one

added theorem Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one

added theorem Finset.affineCombination_filter_of_ne

added theorem Finset.affineCombination_indicator_subset

added theorem Finset.affineCombination_linear

added theorem Finset.affineCombination_map

added theorem Finset.affineCombination_of_eq_one_of_eq_zero

added theorem Finset.affineCombination_sdiff_sub

added theorem Finset.affineCombination_subtype_eq_filter

added theorem Finset.affineCombination_vsub

added theorem Finset.attach_affineCombination_coe

added theorem Finset.attach_affineCombination_of_injective

added def Finset.centroid

added def Finset.centroidWeights

added def Finset.centroidWeightsIndicator

added theorem Finset.centroidWeightsIndicator_def

added theorem Finset.centroidWeights_apply

added theorem Finset.centroidWeights_eq_const

added theorem Finset.centroid_def

added theorem Finset.centroid_eq_affineCombination_fintype

added theorem Finset.centroid_eq_centroid_image_of_inj_on

added theorem Finset.centroid_eq_of_inj_on_of_image_eq

added theorem Finset.centroid_map

added theorem Finset.centroid_pair

added theorem Finset.centroid_pair_fin

added theorem Finset.centroid_singleton

added theorem Finset.centroid_univ

added theorem Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype

added theorem Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype

added theorem Finset.eq_weightedVSub_subset_iff_eq_weightedVSub_subtype

added theorem Finset.map_affineCombination

added theorem Finset.sum_affineCombinationLineMapWeights

added theorem Finset.sum_affineCombinationSingleWeights

added theorem Finset.sum_centroidWeightsIndicator

added theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one

added theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero

added theorem Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty

added theorem Finset.sum_centroidWeights_eq_one_of_card_eq_add_one

added theorem Finset.sum_centroidWeights_eq_one_of_card_ne_zero

added theorem Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero

added theorem Finset.sum_centroidWeights_eq_one_of_nonempty

added theorem Finset.sum_smul_const_vsub_eq_neg_weightedVSub

added theorem Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint

added theorem Finset.sum_smul_const_vsub_eq_vsub_affineCombination

added theorem Finset.sum_smul_vsub_const_eq_affineCombination_vsub

added theorem Finset.sum_smul_vsub_const_eq_weightedVSub

added theorem Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub

added theorem Finset.sum_smul_vsub_eq_affineCombination_vsub

added theorem Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub

added theorem Finset.sum_smul_vsub_eq_weightedVSub_sub

added theorem Finset.sum_weightedVSubVSubWeights

added theorem Finset.univ_fin2

added def Finset.weightedVSub

added def Finset.weightedVSubOfPoint

added theorem Finset.weightedVSubOfPoint_apply

added theorem Finset.weightedVSubOfPoint_apply_const

added theorem Finset.weightedVSubOfPoint_congr

added theorem Finset.weightedVSubOfPoint_const_smul

added theorem Finset.weightedVSubOfPoint_eq_of_sum_eq_zero

added theorem Finset.weightedVSubOfPoint_eq_of_weights_eq

added theorem Finset.weightedVSubOfPoint_erase

added theorem Finset.weightedVSubOfPoint_filter_of_ne

added theorem Finset.weightedVSubOfPoint_indicator_subset

added theorem Finset.weightedVSubOfPoint_insert

added theorem Finset.weightedVSubOfPoint_map

added theorem Finset.weightedVSubOfPoint_sdiff

added theorem Finset.weightedVSubOfPoint_sdiff_sub

added theorem Finset.weightedVSubOfPoint_subtype_eq_filter

added theorem Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one

added def Finset.weightedVSubVSubWeights

added theorem Finset.weightedVSubVSubWeights_apply_left

added theorem Finset.weightedVSubVSubWeights_apply_of_ne

added theorem Finset.weightedVSubVSubWeights_apply_right

added theorem Finset.weightedVSubVSubWeights_self

added theorem Finset.weightedVSub_apply

added theorem Finset.weightedVSub_apply_const

added theorem Finset.weightedVSub_congr

added theorem Finset.weightedVSub_const_smul

added theorem Finset.weightedVSub_empty

added theorem Finset.weightedVSub_eq_linear_combination

added theorem Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero

added theorem Finset.weightedVSub_filter_of_ne

added theorem Finset.weightedVSub_indicator_subset

added theorem Finset.weightedVSub_map

added theorem Finset.weightedVSub_sdiff

added theorem Finset.weightedVSub_sdiff_sub

added theorem Finset.weightedVSub_subtype_eq_filter

added theorem Finset.weightedVSub_vadd_affineCombination

added theorem Finset.weightedVSub_weightedVSubVSubWeights

added theorem affineCombination_mem_affineSpan

added theorem affineSpan_eq_affineSpan_lineMap_units

added theorem centroid_mem_affineSpan_of_card_eq_add_one

added theorem centroid_mem_affineSpan_of_card_ne_zero

added theorem centroid_mem_affineSpan_of_cast_card_ne_zero

added theorem centroid_mem_affineSpan_of_nonempty

added theorem eq_affineCombination_of_mem_affineSpan

added theorem eq_affineCombination_of_mem_affineSpan_of_fintype

added theorem mem_affineSpan_iff_eq_affineCombination

added theorem mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd

added theorem mem_vectorSpan_iff_eq_weightedVSub

added theorem weightedVSub_mem_vectorSpan