English
If G is a group acting on a module, and the action is compatible with the scalar structure, then multiplying a linearly independent family by a G-valued function preserves linear independence.
Русский
Если группа действует на модуль, и действие совместимо со скалярами, то умножение независимого семейства функцией из G сохраняет независимость.
LaTeX
$$LinearIndependent R v → ∀ w : ι → G, LinearIndependent R (w • v)$$
Lean4
theorem group_smul {G : Type*} [hG : Group G] [MulAction G R] [SMul G M] [IsScalarTower G R M] [SMulCommClass G R M]
{v : ι → M} (hv : LinearIndependent R v) (w : ι → G) : LinearIndependent R (w • v) :=
by
rw [linearIndependent_iff''ₛ] at hv ⊢
intro s g₁ g₂ hgs hsum i
refine (Group.isUnit (w i)).smul_left_cancel.mp ?_
refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i
· simp_rw [hgs i hi]
· simpa only [smul_assoc, smul_comm] using hsum
