coeSubmodule_mul — Mathlib

English

The image of the product of two ideals is the product of their images: coeSubmodule(S, I·J) = coeSubmodule(S,I) · coeSubmodule(S,J).

Русский

Образ произведения двух идеалов равен произведению их образов.

LaTeX

$$coeSubmodule_mul : coeSubmodule S (I * J) = coeSubmodule S I * coeSubmodule S J$$

Lean4

@[simp]
theorem coeSubmodule_mul (I J : Ideal R) : coeSubmodule S (I * J) = coeSubmodule S I * coeSubmodule S J :=
  Submodule.map_mul _ _ (Algebra.ofId R S)

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