mem_or_mem

Mathlib.RingTheory.Ideal.Prime

URI: https://scilib.ai/kg/mathlib#Ideal.IsPrime.mem_or_mem

English

If x·y ∈ I for a prime ideal I, then x ∈ I or y ∈ I.

Русский

Если x y ∈ I для простого идеала I, то x ∈ I или y ∈ I.

LaTeX

$$$x y \in I \Rightarrow x \in I \lor y \in I$$$

Lean4

theorem mem_or_mem {I : Ideal α} (hI : I.IsPrime) {x y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I :=
  hI.2

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

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

Разделы

Аффилиация

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