English
If a Finset t has cardinality larger than finrank R M, there exists a nontrivial linear relation among its elements.
Русский
Если множество t имеет размер больше чем finrank R M, существует ненулевая линейная зависимость между его элементами.
LaTeX
$$$t \subseteq M,\; \text{finrank } R M < \lvert t \rvert \Rightarrow \exists f:\, M \to R,\; \sum_{e \in t} f(e)\,e = 0 \land \exists x \in t, f(x) \neq 0$$$
Lean4
/-- If a finset has cardinality larger than the rank of a module,
then there is a nontrivial linear relation amongst its elements. -/
theorem exists_nontrivial_relation_of_finrank_lt_card {t : Finset M} (h : finrank R M < t.card) :
∃ f : M → R, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0 :=
by
obtain ⟨g, sum, z, nonzero⟩ :=
Fintype.not_linearIndependent_iff.mp (mt LinearIndependent.finset_card_le_finrank h.not_ge)
refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩
rw [← Finset.sum_finset_coe]; convert sum; apply Subtype.val_injective.extend_apply
