mem_or_mem_of_mul_eq_zero

Mathlib.RingTheory.Ideal.Prime

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_or_mem_of_mul_eq_zero {I : Ideal α} (hI : I.IsPrime) {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I :=
  hI.mem_or_mem (h.symm ▸ I.zero_mem)

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

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

Разделы

Аффилиация

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