finrank_zero_iff — Mathlib

English

Let M be an R-module of finite dimension. Then finrank_R(M) = 0 if and only if M is a subsingleton.

Русский

Пусть M — R-модуль конечной размерности. Тогда finrank_R(M) = 0 тогда и только тогда, когда M является подсинглтоном (односоставом).

LaTeX

$$$\\\\operatorname{finrank}_R M = 0 \\\\iff \\\\operatorname{Subsingleton} M.$$$

Lean4

/-- A finite-dimensional space has zero `finrank` iff it is a subsingleton.
This is the `finrank` version of `rank_zero_iff`. -/
theorem finrank_zero_iff [NoZeroSMulDivisors R M] : finrank R M = 0 ↔ Subsingleton M :=
  by
  rw [← rank_zero_iff (R := R), ← finrank_eq_rank]
  norm_cast

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