coeSubmodule_injective — Mathlib

English

The image of the join of two ideals is the join of their 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

theorem coeSubmodule_injective (h : M ≤ nonZeroDivisors R) :
    Function.Injective (coeSubmodule S : Ideal R → Submodule R S) :=
  injective_of_le_imp_le _ fun hl => (coeSubmodule_le_coeSubmodule h).mp hl

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