English
The identity relating the algebra map on the tensor product and the multiplication map holds: the equality of two linear maps as in the statement.
Русский
Справедливость тождества между отображением на тензорном произведении и умножением: равенство двух линейных отображений, как указано.
LaTeX
$$$ (\\mathrm{Algebra.linearMap} \\, R (A \\otimes_R B)) \\circ \\mathrm{LinearMap.mul}'_R R = \\mathrm{TensorProduct}.map (\\mathrm{Algebra.linearMap } R A) (\\mathrm{Algebra.linearMap } R B).$$$
Lean4
theorem linearMap_comp_mul' :
Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R = map (Algebra.linearMap R A) (Algebra.linearMap R B) :=
by
ext
simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, map_tmul,
Algebra.linearMap_apply, map_one, LinearMap.coe_comp, Function.comp_apply, LinearMap.mul'_apply, mul_one,
Algebra.TensorProduct.one_def]
