## Stream: Is there code for X?

### Topic: mul_linear_map

#### Scott Morrison (Jul 27 2020 at 09:24):

Any pointers for multiplication in an algebra as a R-linear map?

import ring_theory.algebra

open_locale tensor_product

lemma mul_linear_map (R : Type*) [comm_semiring R] (A : Type*) [semiring A] [algebra R A] :
A ⊗[R] A →ₗ[R] A := sorry


#### Kenny Lau (Jul 27 2020 at 09:24):

I have A -> A -> A

#### Kenny Lau (Jul 27 2020 at 09:25):

it's algebra.lmul

#### Kenny Lau (Jul 27 2020 at 09:25):

A →ₗ[R] A →ₗ[R] A

#### Kenny Lau (Jul 27 2020 at 09:26):

also it isn't a lemma it's a def

#### Scott Morrison (Jul 27 2020 at 09:31):

Perfect, thanks.

Last updated: May 07 2021 at 23:11 UTC