English
For v: Fin (n+1) → V, linear independence is equivalent to the tail being independent and the last element not in the span of the initial tail range.
Русский
Для v: Fin(n+1) → V независимость эквивалентна тому, что хвост независим и последний элемент не лежит в span начального хвоста.
LaTeX
$$$\operatorname{LinearIndependent}_K v \iff \bigl( \operatorname{LinearIndependent}_K(\operatorname{Fin.init} v) \land v(\operatorname{Fin.last} n) \notin \operatorname{span}_K(\operatorname{range}(\operatorname{Fin.init} v)) \bigr)$$$
Lean4
/-- See `LinearIndependent.fin_cons'` for an uglier version that works if you
only have a module over a semiring. -/
theorem fin_cons {n} {v : Fin n → V} (hv : LinearIndependent K v) (hx : x ∉ Submodule.span K (range v)) :
LinearIndependent K (Fin.cons x v : Fin (n + 1) → V) :=
linearIndependent_fin_cons.2 ⟨hv, hx⟩
