English
Let ι be a finite index set and F a field. For any f: ι → α → F, the span of the range of flip f equals the whole space if and only if f is linearly independent.
Русский
Пусть ι — конечный индексный набор и F — поле. Для любой функции f: ι → α → F, зная, что замена порядка (flip f) охватывает всю пространство, эквивалентно тому, что семейство {f_i} линейно независимо.
LaTeX
$$$$ \\operatorname{span}_F\\big( \\operatorname{range}(\\mathrm{flip} f) \\big) = \\top \\quad \\Longleftrightarrow\\quad \\operatorname{LinearIndependent}_F(f). $$$$
Lean4
theorem span_flip_eq_top_iff_linearIndependent {ι α F} [Finite ι] [Field F] {f : ι → α → F} :
span F (Set.range <| flip f) = ⊤ ↔ LinearIndependent F f :=
by
rw [linearIndependent_iff_ker, ← Submodule.map_eq_top_iff (e := Finsupp.llift F F F ι), ←
Subspace.dualCoannihilator_dualAnnihilator_eq (W := map ..), dualAnnihilator_eq_top_iff]
congr!
rw [SetLike.ext'_iff, map_span, Submodule.coe_dualCoannihilator_span, ← Set.range_comp]
ext
simp [funext_iff, Finsupp.linearCombination, Finsupp.sum, Finset.sum_apply, flip]
