restrictScalars_mul — Mathlib

English

Under restriction of scalars, the product of submodules distributes: (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A.

Русский

При ограничении скалярами произведение подмодулов сохраняет распределение: (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A.

LaTeX

$$$ \text{Submodule.restrictScalars}(A) (I * J) = (\text{Submodule.restrictScalars}(A) I) * (\text{Submodule.restrictScalars}(A) J) $$$

Lean4

theorem restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C]
    [IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C] {I J : Submodule B C} :
    (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A :=
  rfl

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