isRadical_iInf

Mathlib.RingTheory.Ideal.Operations

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

English

If every I(i) is radical, then the infimum is radical.

Русский

Если каждый I(i) радикален, то их infimum радикален.

LaTeX

$$$\\forall i, I(i).IsRadical \\Rightarrow (\\bigwedge_i I(i)).IsRadical$$$

Lean4

theorem isRadical_iInf {ι} (I : ι → Ideal R) (hI : ∀ i, IsRadical (I i)) : IsRadical (⨅ i, I i) :=
  (radical_iInf_le I).trans (iInf_mono hI)

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

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

Разделы

Аффилиация

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