English
For a NoZeroSmulDivisors ring R and suitable M, Module.rank R S = 0 if and only if S = ⊥ for a submodule S of M.
Русский
Для кольца R с NoZeroSmulDivisors и подходящей M, Module.rank_R(S) = 0 тогда и только тогда, когда S = ⊥ для подмодуля S ⊆ M.
LaTeX
$$$$\\\\operatorname{Module.rank}_R S = 0 \\\\iff S = \\\\bot.$$$$
Lean4
/-- See `rank_subsingleton` for the reason that `Nontrivial R` is needed. -/
@[simp]
theorem rank_eq_zero [Nontrivial R] [NoZeroSMulDivisors R M] {S : Submodule R M} : Module.rank R S = 0 ↔ S = ⊥ :=
⟨fun h =>
(Submodule.eq_bot_iff _).2 fun x hx =>
congr_arg Subtype.val <|
((Submodule.eq_bot_iff _).1 <| Eq.symm <| Submodule.bot_eq_top_of_rank_eq_zero h) ⟨x, hx⟩ Submodule.mem_top,
fun h => by rw [h, rank_bot]⟩
