Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_linear_map


view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 27 2020 at 09:24):

I have A -> A -> A

view this post on Zulip Kenny Lau (Jul 27 2020 at 09:25):

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

view this post on Zulip Kenny Lau (Jul 27 2020 at 09:25):

it's algebra.lmul

view this post on Zulip Kenny Lau (Jul 27 2020 at 09:25):

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

view this post on Zulip Kenny Lau (Jul 27 2020 at 09:26):

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

view this post on Zulip Scott Morrison (Jul 27 2020 at 09:31):

Perfect, thanks.


Last updated: May 07 2021 at 23:11 UTC