group_smul_iff — Mathlib

English

For a group action, LinearIndependent R (w • v) is equivalent to LinearIndependent R v.

Русский

При групповом действии независимость сохраняется и эквивалентна: независимость w • v ⇔ независимость v.

LaTeX

$$LinearIndependent R (w • v) ↔ LinearIndependent R v$$

Lean4

@[simp]
theorem group_smul_iff {G : Type*} [hG : Group G] [MulAction G R] [MulAction G M] [IsScalarTower G R M]
    [SMulCommClass G R M] (v : ι → M) (w : ι → G) : LinearIndependent R (w • v) ↔ LinearIndependent R v :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩
  convert h.group_smul (fun i ↦ (w i)⁻¹)
  simp [funext_iff]
    -- This lemma cannot be proved with `LinearIndependent.group_smul` since the action of
    -- `Rˣ` on `R` is not commutative.

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