mem_zeroLocus

Mathlib.RingTheory.Spectrum.Prime.Basic

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.mem_zeroLocus

English

Membership in zeroLocus s is equivalent to containment of s in x.asIdeal.

Русский

Принадлежность элементу в zeroLocus s эквивалентна включению s в x.asIdeal.

LaTeX

$$$x \\in \\operatorname{zeroLocus}(s) \\iff s \\subseteq x.asIdeal$$$

Lean4

@[simp]
theorem mem_zeroLocus (x : PrimeSpectrum R) (s : Set R) : x ∈ zeroLocus s ↔ s ⊆ x.asIdeal :=
  Iff.rfl

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

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

Разделы

Аффилиация

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