not_isAssociatedPrime_of_subsingleton

English

If M is a subsingleton, then there is no associated prime I for M.

Русский

Если модуль M нуль-субоднозначен, то для него не существует ассоциированного простого I.

LaTeX

$$$$ [\text{Subsingleton } M] \Rightarrow \lnot \IsAssociatedPrime I M. $$$$

Lean4

theorem not_isAssociatedPrime_of_subsingleton [Subsingleton M] : ¬IsAssociatedPrime I M :=
  by
  rintro ⟨hI, x, hx⟩
  apply hI.ne_top
  simpa [Subsingleton.elim x 0] using hx

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