notMem_support_iff

Mathlib.RingTheory.Support

URI: https://scilib.ai/kg/mathlib#Module.notMem_support_iff

English

An element p is not in the support if and only if the localized module M_p is the zero module.

Русский

Если p не принадлежит опоре,то локализация M_p равна нулевому модулю.

LaTeX

$$$p \notin \mathrm{Supp}_R(M) \iff M_p = 0$$$

Lean4

theorem notMem_support_iff : p ∉ Module.support R M ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M) :=
  not_nontrivial_iff_subsingleton

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru