English
Let N be a submodule of M over a ring R with NoZeroDivisors. If every finite set of vectors from N which is linearly independent in M must have cardinality zero, then N is the zero submodule.
Русский
Пусть N — подпространство M над кольцом R без нулевых делителей. Если каждая конечная линейно независимая подсистема из N в M пустая, то N равно нулевому подпространству.
LaTeX
$$$[\\text{NoZeroDivisors } R] \\Rightarrow (\\forall N: Submodule\\ R\\ M,\\ (\\forall m:\\mathbb{N},\\forall v: Fin m \\to N,\\ LinearIndependent_R(\\uparrow \\circ v) \\Rightarrow m = 0) \\Rightarrow N = \\bot)$$$
Lean4
theorem eq_bot_of_rank_eq_zero [NoZeroDivisors R] (b : Basis ι R M) (N : Submodule R M)
(rank_eq : ∀ {m : ℕ} (v : Fin m → N), LinearIndependent R ((↑) ∘ v : Fin m → M) → m = 0) : N = ⊥ :=
by
rw [Submodule.eq_bot_iff]
intro x hx
contrapose! rank_eq with x_ne
refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩
rw [Fintype.linearIndependent_iff]
rintro g sum_eq i
obtain ⟨_, hi⟩ := i
simp only [Fin.default_eq_zero, Finset.univ_unique, Finset.sum_singleton] at sum_eq
convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
