Would it be possible to make a channel for iris-lean?

Stream: general

[Markus de Medeiros]

Since there's interest in this project again, it would be great if we had a channel to coordinate (rather than random DM's and emails :sweat_smile:). If nobody else wants to moderate I'd be happy to do it, though I don't have any experience moderating channels on here so might need some guidelines for what to do.

[Mario Carneiro]

if it's a public stream it will get moderation along with everything else from the moderator team (which is also the mathlib maintainer team, more or less)

[Markus de Medeiros]

Oh cool! I read somewhere on here that new channels needed a mod but if not that's even easier

[Mario Carneiro]

#iris-lean

[Mario Carneiro]

that's only for private channels, since they aren't accessible to the mod team unless they are specifically invited

[Markus de Medeiros]

Awesome. Thanks!