## Stream: maths

### Topic: algebra structure on lc

#### Johan Commelin (Mar 21 2019 at 07:29):

If A is an R-algebra, then there is a natural algebra structure on lc R A, which is just "expanding the product". It turns lc.total into an algebra hom. Should this go in mathlib. (I think it is valuable.) If so, where?
https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/lc_algebra.lean

Last updated: May 11 2021 at 16:22 UTC