isPrimary

Mathlib.RingTheory.Ideal.IsPrimary

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

← MathLib Explorer

English

If I is a prime ideal, then I is primary.

Русский

Если I является примарным (prime) идеалом, то он является примарным (primary).

LaTeX

$$IsPrime I ⇒ I.IsPrimary$$

Lean4

theorem isPrimary {I : Ideal R} (hi : IsPrime I) : I.IsPrimary :=
  isPrimary_iff.mpr ⟨hi.1, fun {_ _} hxy => (hi.mem_or_mem hxy).imp id fun hyi => le_radical hyi⟩

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

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

Разделы

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

Аффилиация

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