mem_support_iff — Mathlib

English

A prime p lies in the support of M precisely when the localization M_p is nonzero.

Русский

Простой идеал p принадлежит опоре модуля M тогда и только тогда, когда локализация M_p не тождественно нулевая.

LaTeX

$$$p \in \mathrm{Supp}_R(M) \iff M_p \neq 0$$$

Lean4

theorem mem_support_iff : p ∈ Module.support R M ↔ Nontrivial (LocalizedModule p.asIdeal.primeCompl M) :=
  Iff.rfl

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