linearIndependent_fin2 — Mathlib

English

For f: Fin 2 → V, linear independence is equivalent to f(1) ≠ 0 and for all a ∈ K, a f(1) ≠ f(0).

Русский

Для f: Fin 2 → V независимость эквивалентна f(1) ≠ 0 и для всякого a ∈ K выполняется a f(1) ≠ f(0).

LaTeX

$$$\operatorname{LinearIndependent}_K f \iff \bigl(f(1) \neq 0 \land \forall a \in K, a \cdot f(1) \neq f(0)\bigr)$$$

Lean4

theorem linearIndependent_fin2 {f : Fin 2 → V} : LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ a : K, a • f 1 ≠ f 0 := by
  rw [linearIndependent_fin_succ, linearIndependent_unique_iff, range_unique, mem_span_singleton, not_exists,
    show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]

Похожие утверждения