eq_empty_of_subsingleton — Mathlib

English

If the module M is a subsingleton (has at most one element), then Ass_R(M) = ∅.

Русский

Если модуль M является подсинглотоном (имеет не более одного элемента), то Ass_R(M) = ∅.

LaTeX

$$$(\\operatorname{Ass}_R(M)) = \\varnothing$ если $M$ — subsingleton.$$

Lean4

theorem eq_empty_of_subsingleton [Subsingleton M] : associatedPrimes R M = ∅ :=
  by
  ext; simp only [Set.mem_empty_iff_false, iff_false]
  apply not_isAssociatedPrime_of_subsingleton

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