prod_mono_right

Mathlib.RingTheory.Ideal.Prod

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

English

If J1 ⊆ J2 are ideals of S, then I ⋅ J1 ⊆ I ⋅ J2 for any ideal I of R.

Русский

Если J1 ⊆ J2 для идеалов S, то I ⋅ J1 ⊆ I ⋅ J2 для любого идеала I в R.

LaTeX

$$$J_1 \\le J_2 \\Rightarrow I \\mathrm{prod} J_1 \\le I \\mathrm{prod} J_2$$$

Lean4

theorem prod_mono_right {I : Ideal R} {J₁ J₂ : Ideal S} (hJ : J₁ ≤ J₂) : prod I J₁ ≤ prod I J₂ :=
  Set.prod_mono_right hJ

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

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

Разделы

Аффилиация

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