length_eq_zero_iff — Mathlib

English

The length is zero iff the module is subsingleton; equivalently, length equals zero exactly when the submodule lattice has no nontrivial elements.

Русский

Длина равна нулю тогда и только тогда, когда модуль является подсубмодулем (соответственно, решетка подмодулов тривиальна).

LaTeX

$$$\operatorname{length}(R,M) = 0 \iff \operatorname{Subsingleton} M.$$$

Lean4

theorem length_eq_zero_iff : Module.length R M = 0 ↔ Subsingleton M := by
  rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero, Order.krullDim_eq_zero_iff_of_orderTop,
    Submodule.subsingleton_iff]

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