English
A variant form: the equality rank R M = 0 holds exactly when every element x ∈ M satisfies ∃ a ≠ 0 with a·x = 0.
Русский
Вариант: ранг равен нулю тогда и только тогда для каждого x ∈ M существует a ≠ 0 с a·x = 0.
LaTeX
$$$\operatorname{rank}_R M = 0 \iff \forall x \in M,\; \exists a \in R,\; a \neq 0 \land a\cdot x = 0.$$$
Lean4
/-- See `rank_zero_iff` for a stronger version with `NoZeroSMulDivisor R M`. -/
theorem rank_eq_zero_iff : Module.rank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 :=
by
nontriviality R
constructor
· contrapose!
rintro ⟨x, hx⟩
rw [← Cardinal.one_le_iff_ne_zero]
have : LinearIndependent R (fun _ : Unit ↦ x) :=
linearIndependent_iff.mpr
(fun l hl ↦
Finsupp.unique_ext <| not_not.mp fun H ↦ hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))
simpa using this.cardinal_lift_le_rank
· intro h
rw [← le_zero_iff, Module.rank_def]
apply ciSup_le'
intro ⟨s, hs⟩
rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]
rintro ⟨i : s⟩
obtain ⟨a, ha, ha'⟩ := h i
apply ha
simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i
