prod_mono — Mathlib

English

If I1 ⊆ I2 are ideals of R and J1 ⊆ J2 are ideals of S, then I1 ⋅ J1 ⊆ I2 ⋅ J2 in R × S.

Русский

Если I1 ⊆ I2 и J1 ⊆ J2 для замкнутых по умножению идеалов R и S, то I1.prod J1 ⊆ I2.prod J2 в R × S.

LaTeX

$$$I_1 \\le I_2 \\rightarrow J_1 \\le J_2 \\rightarrow I_1 \\mathrm{prod} J_1 \\le I_2 \\mathrm{prod} J_2$$$

Lean4

@[gcongr]
theorem prod_mono {I₁ I₂ : Ideal R} {J₁ J₂ : Ideal S} (hI : I₁ ≤ I₂) (hJ : J₁ ≤ J₂) : prod I₁ J₁ ≤ prod I₂ J₂ :=
  Set.prod_mono hI hJ

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