mul_notMem

Mathlib.RingTheory.Ideal.Prime

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

English

If x ∉ I and y ∉ I for a prime ideal I, then x y ∉ I.

Русский

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

LaTeX

$$x \notin I \land y \notin I \Rightarrow x y \notin I$$

Lean4

theorem mul_notMem {I : Ideal α} (hI : I.IsPrime) {x y : α} : x ∉ I → y ∉ I → x * y ∉ I := fun hx hy h ↦
  hy ((hI.mem_or_mem h).resolve_left hx)

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

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

Разделы

Аффилиация

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