mem_primeCompl_iff

Mathlib.RingTheory.Ideal.Prime

URI: https://scilib.ai/kg/mathlib#Ideal.mem_primeCompl_iff

English

For a prime ideal P, x ∈ P.primeCompl iff x ∉ P.

Русский

Для простого идеала P, x ∈ P.primeCompl тогда и только тогда x ∉ P.

LaTeX

$$x \in P.primeCompl \iff x \notin P$$

Lean4

@[simp]
theorem mem_primeCompl_iff {P : Ideal α} [P.IsPrime] {x : α} : x ∈ P.primeCompl ↔ x ∉ P :=
  Iff.rfl

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

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

Разделы

Аффилиация

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