English
If e is a bijection between index sets, then AffineIndependent k (p ∘ e) is equivalent to AffineIndependent k p.
Русский
Если e — биекция между множителями индексов, то аффинная независимость сохраняется под композицией p ∘ e и p.
LaTeX
$$AffineIndependent k (p ∘ e) ↔ AffineIndependent k p$$
Lean4
/-- If we single out one member of an affine-independent family of points and affinely transport
all others along the line joining them to this member, the resulting new family of points is affine-
independent.
This is the affine version of `LinearIndependent.units_smul`. -/
theorem units_lineMap {p : ι → P} (hp : AffineIndependent k p) (j : ι) (w : ι → Units k) :
AffineIndependent k fun i => AffineMap.lineMap (p j) (p i) (w i : k) :=
by
rw [affineIndependent_iff_linearIndependent_vsub k _ j] at hp ⊢
simp only [AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same, const_apply]
exact hp.units_smul fun i => w i
