English
A family is dependent if and only if their representatives are linearly dependent.
Русский
Семейство зависимо тогда и только тогда, когда представленные ими векторы линейно зависимы.
LaTeX
$$$Dependent(f) \\iff \\lnot LinearIndependent(K, (Projectivization.rep \\circ f))$$$
Lean4
/-- A family of points in a projective space is dependent if and only if their
representatives are linearly dependent. -/
theorem dependent_iff : Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f) :=
by
refine ⟨?_, fun h => ?_⟩
· rintro ⟨ff, hff, hh1⟩
contrapose! hh1
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
convert hh1.units_smul a⁻¹
ext i
simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]
· convert Dependent.mk _ _ h
· simp only [mk_rep, Function.comp_apply]
· exact fun i => rep_nonzero (f i)
