weightedVSubOfPoint_smul — Mathlib

English

If a group G acts on V and K and acts compatibly with the scalar structure, then s.weightedVSubOfPoint (a • p) b w = a • s.weightedVSubOfPoint p (a^{-1} • b) w.

Русский

Пусть группа G действует на V совместимо со скалярами; тогда s.weightedVSubOfPoint (a⋅p) b w = a ⋅ s.weightedVSubOfPoint p (a^{-1}⋅b) w.

LaTeX

$$$ s.weightedVSubOfPoint (a \\cdot p) b w = a \\cdot s.weightedVSubOfPoint p (a^{-1} \\cdot b) w $$$

Lean4

theorem weightedVSubOfPoint_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] (s : Finset ι)
    (w : ι → k) (p : ι → V) (b : V) (a : G) :
    s.weightedVSubOfPoint (a • p) b w = a • s.weightedVSubOfPoint p (a⁻¹ • b) w := by
  simp [smul_sum, smul_sub, smul_comm a (w _)]

Похожие утверждения