English
If ι is finite, then AffineIndependent k p is equivalent to a condition on all weight functions w: ι → k expressed via univ and weightedVSub.
Русский
Если ι конечно, аффинная независимость k-переменной p эквивалентна условию на все весовые функции w: ι → k, записываемому через univ и weightedVSub.
LaTeX
$$$\text{AffineIndependent}_k(p) \iff \forall w:\ ι \to k, \sum_i w_i = 0 \to \text{univ.weightedVSub } p \ w = 0 \to \forall i, w_i = 0$$$
Lean4
/-- A family indexed by a `Fintype` is affinely independent if and
only if no nontrivial weighted subtractions over `Finset.univ` (where
the sum of the weights is 0) are 0. -/
theorem affineIndependent_iff_of_fintype [Fintype ι] (p : ι → P) :
AffineIndependent k p ↔ ∀ w : ι → k, ∑ i, w i = 0 → Finset.univ.weightedVSub p w = (0 : V) → ∀ i, w i = 0 :=
by
constructor
· exact fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _)
· intro h s w hw hs i hi
rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs
rw [← Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw
replace h := h ((↑s : Set ι).indicator w) hw hs i
simpa [hi] using h
