mul_linear_map

Stream: Is there code for X?

[Scott Morrison]

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]

I have A -> A -> A

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/229cf6ef21126e17e6ec78b4acc5413ad0a8a02d/src/ring_theory/algebra.lean#L182

[Kenny Lau]

it's algebra.lmul

[Kenny Lau]

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

[Kenny Lau]

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

[Scott Morrison]

Perfect, thanks.