rank_zero_iff — Mathlib

English

Over a ring R with appropriate hypotheses, rank zero is equivalent to the underlying module M being a subsingleton.

Русский

При надлежащих условиях размерность нуль эквивалентна тому, что модуль M является подпредставлением (subs), т.е. subsingleton.

LaTeX

$$$\operatorname{rank}_R M = 0 \iff M \text{ is subsingleton}.$$$

Lean4

/-- See `rank_subsingleton` for the reason that `Nontrivial R` is needed.
Also see `rank_eq_zero_iff` for the version without `NoZeroSMulDivisor R M`. -/
theorem rank_zero_iff : Module.rank R M = 0 ↔ Subsingleton M :=
  rank_zero_iff_forall_zero.trans (subsingleton_iff_forall_eq 0).symm

Похожие утверждения