Centroids under affine and linear maps

[UPSTREAM] Affine maps commute with the centroids of nonempty finite families of points, the centroid case of Finset.map_affineCombination; so do linear maps, a module being an affine space over itself; and in a module the centroid is the average of the points.

theorem Finset.map_centroid_of_cast_card_ne_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {ι : Type u_6} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (s : Finset ι) (p : ι → P) (f : P →ᵃ[k] P₂) (h : ↑s.card ≠ 0) : f (centroid k s p) = centroid k s (⇑f ∘ p)

Affine maps commute with centroids, if the number of points, converted to k, is not zero.

theorem Finset.map_centroid_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {ι : Type u_6} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (s : Finset ι) [CharZero k] (p : ι → P) (f : P →ᵃ[k] P₂) (h : s.Nonempty) : f (centroid k s p) = centroid k s (⇑f ∘ p)

In the characteristic zero case, affine maps commute with centroids of nonempty sets.

theorem Finset.centroid_eq_smul_sum {k : Type u_1} {V : Type u_2} {ι : Type u_6} [DivisionRing k] [AddCommGroup V] [Module k V] (s : Finset ι) (p : ι → V) (h : ↑s.card ≠ 0) : centroid k s p = (↑s.card)⁻¹ • ∑ i ∈ s, p i

The centroid of points of a module is their average, if the number of points, converted to k, is not zero.

theorem LinearMap.map_centroid {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {ι : Type u_4} [DivisionRing k] [CharZero k] [AddCommGroup V] [Module k V] [AddCommGroup V₂] [Module k V₂] (f : V →ₗ[k] V₂) {s : Finset ι} (h : s.Nonempty) (p : ι → V) : f (Finset.centroid k s p) = Finset.centroid k s (⇑f ∘ p)

In the characteristic zero case, linear maps commute with centroids of nonempty sets.