English
The product of two ideals, when restricted to scalars, equals the product of their restrictions: (I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R.
Русский
Произведение идеалов после ограничения скаляров равно произведению их ограничений: (I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R.
LaTeX
$$$ (I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R $$$
Lean4
/-- The smallest `S`-submodule that contains all `x ∈ I * y ∈ J`
is also the smallest `R`-submodule that does so. -/
@[simp]
theorem restrictScalars_mul {R S : Type*} [Semiring R] [Semiring S] [Module R S] [IsScalarTower R S S] (I J : Ideal S) :
(I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R :=
rfl
