inf

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.IsRadical.inf

English

If I and J are radical, then I ∩ J is radical.

Русский

Если I и J радикальны, то I ∩ J радикален.

LaTeX

$$$I.IsRadical \\to J.IsRadical \\Rightarrow (I \\cap J).IsRadical$$$

Lean4

theorem inf (hI : IsRadical I) (hJ : IsRadical J) : IsRadical (I ⊓ J) := by rw [IsRadical, radical_inf];
  exact inf_le_inf hI hJ

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

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

Разделы

Аффилиация

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