toIdeal_inf

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#HomogeneousIdeal.toIdeal_inf

English

The toIdeal map preserves inf: (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal.

Русский

Отображение toIdeal сохраняет инф: (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal.

LaTeX

$$$(I \\cap J).toIdeal = I.toIdeal \\cap J.toIdeal$$$

Lean4

@[simp]
theorem toIdeal_inf (I J : HomogeneousIdeal 𝒜) : (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal :=
  rfl

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

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

Разделы

Аффилиация

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