isZero_of_iff_subsingleton — Mathlib

English

For a module M, IsZero of the corresponding ModuleCat object is equivalent to M being a subsingleton.

Русский

Для модуля M из ModuleCat равносильно IsZero соответствующего объекта равносильно тому, что M является subsingleton.

LaTeX

$$$\text{IsZero}(\text{ModuleCat}.of\ R\ M) \iff \text{Subsingleton}(M)$$$

Lean4

@[simp]
theorem isZero_of_iff_subsingleton {M : Type*} [AddCommGroup M] [Module R M] : IsZero (of R M) ↔ Subsingleton M :=
  isZero_iff_subsingleton

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