algebra structure on `lc`

Stream: maths

[Johan Commelin]

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