inf

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

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

English

The intersection of two homogeneous ideals is homogeneous.

Русский

Пересечение двух однородных идеалов однородно.

LaTeX

$$$(I \\cap J).IsHomogeneous 𝒜$ given $I.IsHomogeneous 𝒜$ and $J.IsHomogeneous 𝒜$.$$

Lean4

theorem inf {I J : Ideal A} (HI : I.IsHomogeneous 𝒜) (HJ : J.IsHomogeneous 𝒜) : (I ⊓ J).IsHomogeneous 𝒜 := fun _ _ hr =>
  ⟨HI _ hr.1, HJ _ hr.2⟩

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

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

Разделы

Аффилиация

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