Binary Tower Fin 2 Linear Independence

Linear-independence lemmas specialized to functions indexed by Fin 2.

theorem linearIndependent_fin2' {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Fin 2 → V} : LinearIndependent K f ↔ f 0 ≠ 0 ∧ ∀ (a : K), a • f 0 ≠ f 1