English
The smul of a sum in A by the tensor product module is distributive over the tensor product structure, aligning with the algebraic rules for moduleAux.
Русский
Дистрибутивность скаляра слева и справа в moduleAux согласуется с правилами модуля.
LaTeX
$$moduleAux (x + y) m = moduleAux x m + moduleAux y m$$
Lean4
/-- An auxiliary definition, used for constructing the `Module (A ⊗[R] B) M` in
`TensorProduct.Algebra.module` below. -/
def moduleAux : A ⊗[R] B →ₗ[R] M →ₗ[R] M :=
TensorProduct.lift
{ toFun := fun a => a • (Algebra.lsmul R R M : B →ₐ[R] Module.End R M).toLinearMap
map_add' := fun r t => by
ext
simp only [add_smul, LinearMap.add_apply]
map_smul' := fun n r => by
ext
simp only [RingHom.id_apply, LinearMap.smul_apply, smul_assoc] }
