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