coeSubmodule_sup — Mathlib

English

The image of the join of two ideals is the join of the images: coeSubmodule(S, I ⊔ J) = coeSubmodule(S,I) ⊔ coeSubmodule(S,J).

Русский

Образ суммы двух идеалов равен сумме их образов.

LaTeX

$$coeSubmodule_sup : coeSubmodule S (I ⊔ J) = coeSubmodule S I ⊔ coeSubmodule S J$$

Lean4

@[simp]
theorem coeSubmodule_sup (I J : Ideal R) : coeSubmodule S (I ⊔ J) = coeSubmodule S I ⊔ coeSubmodule S J :=
  Submodule.map_sup _ _ _

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