Group (/monoid) rings

Stream: Is there code for X?

[Daan van Gent]

I cannot seem to find a group rings in lean. Should something like

variables (R M : Type*) [ring R] [monoid M]

def monoid_ring := ⨁ m : M, R

instance add_comm_group_monoid_ring : add_comm_group (monoid_ring R M) := direct_sum.add_comm_group _
instance module_monoid_ring : module R (monoid_ring R M) := direct_sum.module
instance monoid_monoid_ring : monoid (monoid_ring R M) := sorry
instance ring_monoid_ring : ring (monoid_ring R M) := sorry
instance algebra_monoid_ring [comm_ring R]: algebra R (monoid_ring R M) := sorry

be added somewhere?

[Yaël Dillies]

cc @Amelia Livingston

[Anatole Dedecker]

Isn’t it docs#monoid_algebra ?

[Daan van Gent]

I see. Thanks! Now i feel silly for not searching for trying that search query.

[Anatole Dedecker]

No problem, this is the purpose of this stream!

[Eric Wieser]

Your spelling should work too if you import algebra.direct_sum.ring

[Eric Wieser]

docs#direct_sum.ring