isPrime_ideal_prod_top

Mathlib.RingTheory.Ideal.Prod

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

← MathLib Explorer

English

For any prime I ⊆ S, the ideal ⊤ × I is prime in R × S.

Русский

Для любого простого I в S, ⊤ × I простый в R × S.

LaTeX

$$$(\\top) \\mathrm{prod} I \\text{ IsPrime}$$$

Lean4

theorem isPrime_ideal_prod_top {I : Ideal R} [h : I.IsPrime] : (prod I (⊤ : Ideal S)).IsPrime
    where
  ne_top' := by simpa using h.ne_top
  mem_or_mem' {x y} := by simpa using h.mem_or_mem

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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