algHomOfLinearMapTensorProduct_apply

English

The applied algebra morphism from algHomOfLinearMapTensorProduct acts by applying the underlying linear map to the input tensor.

Русский

Применённый алгебра-гомоморфизм из algHomOfLinearMapTensorProduct действует через линейное отображение на входной тензор.

LaTeX

$$$(\text{algHomOfLinearMapTensorProduct } f h_{mul} h_{one})(x)=f(x)$$$

Lean4

@[simp]
theorem algHomOfLinearMapTensorProduct_apply (f h_mul h_one x) :
    (algHomOfLinearMapTensorProduct f h_mul h_one : A ⊗[R] B →ₐ[S] C) x = f x :=
  rfl

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