notMem_support_iff' — Mathlib

English

A prime p is not in the support if and only if for every m in M there exists r outside p that annihilates m.

Русский

Пусть p не принадлежит опоре; тогда для каждого m ∈ M найдется r ∉ p, такой что r m = 0.

LaTeX

$$$p \notin \mathrm{Supp}_R(M) \iff \forall m \in M, \exists r \notin \mathfrak p,\; r m = 0$$$

Lean4

theorem notMem_support_iff' : p ∉ Module.support R M ↔ ∀ m : M, ∃ r ∉ p.asIdeal, r • m = 0 := by
  simp only [notMem_support_iff, Ideal.primeCompl, LocalizedModule.subsingleton_iff, Submonoid.mem_mk,
    Subsemigroup.mem_mk, Set.mem_compl_iff, SetLike.mem_coe]

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