affineIndependent_smul — Mathlib

English

If p is affinely independent and G acts on V by a group action, then a ⋅ p is affinely independent iff p is.

Русский

Если p аффинно независимо, и группа действует на V, тогда a⋅p аффинно независимо тогда и только тогда, когда p независимо.

LaTeX

$$$\text{AffineIndependent}_k(p) \iff \text{AffineIndependent}_k(a\cdot p)$$$

Lean4

@[simp]
theorem affineIndependent_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G} :
    AffineIndependent k (a • p) ↔ AffineIndependent k p := by
  simp +contextual [AffineIndependent, ← smul_comm (α := V) a, ← smul_sum, smul_eq_zero_iff_eq]

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